-- Mathlib/Order/LatticeIntervals.lean
protected lemma complementedLattice_iff [Lattice α] [BoundedOrder α] :
    ComplementedLattice (Iic a) ↔ ∀ b, b ≤ a → ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Proof state:
case refine_1.intro.mk
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ComplementedLattice ↑(Iic a)
b : α
hb : b ≤ a
c : α
hc₁ : c ∈ Iic a
hc : IsCompl ⟨b, hb⟩ ⟨c, hc₁⟩
⊢ ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
obtain ⟨hc₂, hc₃⟩ := Set.Iic.isCompl_iff.mp hc

Result:
case refine_1.intro.mk.intro
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ComplementedLattice ↑(Iic a)
b : α
hb : b ≤ a
c : α
hc₁ : c ∈ Iic a
hc : IsCompl ⟨b, hb⟩ ⟨c, hc₁⟩
hc₂ : Disjoint ↑⟨b, hb⟩ ↑⟨c, hc₁⟩
hc₃ : ↑⟨b, hb⟩ ⊔ ↑⟨c, hc₁⟩ = a
⊢ ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Proof state:
case refine_1
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ComplementedLattice ↑(Iic a)
b : α
hb : b ≤ a
⊢ ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
obtain ⟨⟨c, hc₁⟩, hc⟩ := exists_isCompl (⟨b, hb⟩ : Iic a)

Result:
case refine_1.intro.mk
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ComplementedLattice ↑(Iic a)
b : α
hb : b ≤ a
c : α
hc₁ : c ∈ Iic a
hc : IsCompl ⟨b, hb⟩ ⟨c, hc₁⟩
⊢ ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
c : α
hc₁ : c ≤ a
hc₂ : x ⊓ c = ⊥
hc₃ : x ⊔ c = a
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = a

Tactic:
exact ⟨⟨c, hc₁⟩, disjoint_iff.mpr hc₂, hc₃⟩

Result:
no goals

Proof state:
case refine_1.intro.mk.intro
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ComplementedLattice ↑(Iic a)
b : α
hb : b ≤ a
c : α
hc₁ : c ∈ Iic a
hc : IsCompl ⟨b, hb⟩ ⟨c, hc₁⟩
hc₂ : Disjoint ↑⟨b, hb⟩ ↑⟨c, hc₁⟩
hc₃ : ↑⟨b, hb⟩ ⊔ ↑⟨c, hc₁⟩ = a
⊢ ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
exact ⟨c, hc₁, disjoint_iff.mp hc₂, hc₃⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Tactic:
simp_rw [Set.Iic.isCompl_iff]

Result:
case refine_2
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = a

Proof state:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
⊢ ComplementedLattice ↑(Iic a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
refine ⟨fun h b hb ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ↦ ?_⟩⟩

Result:
case refine_1
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ComplementedLattice ↑(Iic a)
b : α
hb : b ≤ a
⊢ ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

case refine_2
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, IsCompl ⟨x, hx⟩ b

Proof state:
case refine_2
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = a

Tactic:
obtain ⟨c, hc₁, hc₂, hc₃⟩ := h x hx

Result:
case refine_2.intro.intro.intro
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
h : ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
x✝ : ↑(Iic a)
x : α
hx : x ∈ Iic a
c : α
hc₁ : c ≤ a
hc₂ : x ⊓ c = ⊥
hc₃ : x ⊔ c = a
⊢ ∃ b, Disjoint x ↑b ∧ x ⊔ ↑b = a