conditionally complete lattice structure on with_top(conditionally complete lattice)

with_top.conditionally_complete_lattice.lean

import order.conditionally_complete_lattice

open lattice

open_locale classical

/- with_top -/

noncomputable instance with_top.conditionally_complete_lattice.has_Sup
  {α : Type*} [conditionally_complete_lattice α] : has_Sup (with_top α) :=
⟨λ S, if ⊤ ∈ S then ⊤ else
      let So := (coe ⁻¹' S : set α) in
      if bdd_above So then ↑(Sup So) else ⊤⟩

noncomputable instance with_top.conditionally_complete_lattice.has_Inf
  {α : Type*} [conditionally_complete_lattice α] : has_Inf (with_top α) :=
⟨λ S, if S ⊆ {⊤} then ⊤ else ↑(Inf (coe ⁻¹' S) : α)⟩

noncomputable instance {α : Type*} [conditionally_complete_lattice α] :
  conditionally_complete_lattice (with_top α) :=
{ le_cSup := λ S a hS haS,
    let So := (coe ⁻¹' S : set α) in
    show a ≤ (ite (⊤ ∈ S) ⊤ (ite (bdd_above So) ↑(Sup So) ⊤)),
    begin split_ifs,
    { exact le_top},
    { cases a, contradiction, exact with_top.some_le_some.2 (le_cSup h_1 haS)},
    { exact le_top},
    end,
  cSup_le := λ S a hS haS,
    let So := (coe ⁻¹' S : set α) in
    show (ite (⊤ ∈ S) ⊤ (ite (bdd_above So) ↑(Sup So) ⊤)) ≤ a,
    begin split_ifs,
    { exact haS h},
    { cases a, exact le_top, apply with_top.some_le_some.2,
      refine cSup_le _ _,
      { intro h1, apply hS, ext x, cases x, simpa using h, show So x ↔ _, rw h1, refl},
      { intros b hb, exact with_top.some_le_some.1 (haS hb)}
    },
    { cases a, exact le_refl _,
      exfalso, apply h_1, use a, intros b hb, exact with_top.some_le_some.1 (haS hb)},
    end,
  cInf_le := λ S a hS haS,
    show (ite (S ⊆ {⊤}) ⊤ ↑(Inf (coe ⁻¹' S))) ≤ a,
    begin
    cases a, exact le_top,
    split_ifs,
    { rcases (h haS) with ⟨⟨⟩⟩, cases h_1},
    { refine with_top.some_le_some.2 (cInf_le _ haS),
      cases hS with a ha,
      cases a with a,
      { use a, intros b hb, exact false.elim (with_top.not_top_le_coe b (ha hb))},
      { use a, intros b hb, refine with_top.some_le_some.1 (ha hb)}
    }
  end,
  le_cInf := λ S a hS haS,
    show a ≤ (ite (S ⊆ {⊤}) ⊤ ↑(Inf (coe ⁻¹' S))),
    begin
    cases a with a,
    { split_ifs, exact le_refl _,
      exfalso, apply h, intros s hs, simpa using top_le_iff.1 (haS hs),
    },
    { split_ifs, exact le_top,
      refine with_top.some_le_some.2 (le_cInf _ _),
      { intro h2, apply h, intros a ha, cases a, left, refl,
          exfalso, apply set.not_mem_empty a_1, rw ←h2, exact ha
      },
      { intros b hb, exact with_top.some_le_some.1 (haS hb) }
    },
  end,
  ..with_top.lattice,
  ..with_top.conditionally_complete_lattice.has_Sup,
  ..with_top.conditionally_complete_lattice.has_Inf
}