-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem Iic_coatomic_of_compact_element {k : α} (h : IsCompactElement k) :
    IsCoatomic (Set.Iic k)

Proof state:
case eq_top_or_exists_le_coatom.mk.inl.h.a
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ↑⟨b, hbk⟩ = ↑⊤

Tactic:
simp only [Set.Iic.coe_top, Subtype.coe_mk]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S

Tactic:
apply le_sSup

Result:
no goals

Proof state:
case eq_top_or_exists_le_coatom.mk
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
obtain rfl | H := eq_or_ne b k

Result:
case eq_top_or_exists_le_coatom.mk.inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

case eq_top_or_exists_le_coatom.mk.inr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
⊢ IsCoatomic ↑(Iic k)

Tactic:
constructor

Result:
case eq_top_or_exists_le_coatom
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
⊢ ∀ (b : ↑(Iic k)), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Proof state:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∀ c ⊆ Iio k, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ Iio k, ∀ z ∈ c, z ≤ ub

Tactic:
intro S SC cC I _

Result:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Proof state:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
refine ⟨sSup S, h.directed_sSup_lt_of_lt hS cC.directedOn SC, ?_⟩

Result:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∀ z ∈ S, z ≤ sSup S

Proof state:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
by_cases hS : S.Nonempty

Result:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

case neg
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Proof state:
case eq_top_or_exists_le_coatom.mk.inl.h
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤

Tactic:
ext

Result:
case eq_top_or_exists_le_coatom.mk.inl.h.a
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ↑⟨b, hbk⟩ = ↑⊤

Proof state:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun x => x ∈ Iio k) a
⊢ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
refine ⟨⟨a, le_of_lt h.prop⟩, ⟨ne_of_lt h.prop, fun c hck => by_contradiction fun c₀ => ?_⟩, ba⟩

Result:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun x => x ∈ Iio k) a
c : ↑(Iic k)
hck : ⟨a, ⋯⟩ < c
c₀ : ¬c = ⊤
⊢ False

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∀ z ∈ S, z ≤ b

Tactic:
simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
  forall_prop_of_false, not_false_iff]

Result:
no goals

Proof state:
case eq_top_or_exists_le_coatom.mk.inr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
right

Result:
case eq_top_or_exists_le_coatom.mk.inr.h
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Proof state:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
⊢ ∀ z ∈ S, z ≤ sSup S

Tactic:
intro

Result:
case pos
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : S.Nonempty
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S

Proof state:
case eq_top_or_exists_le_coatom.mk.inr.h
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
have ⟨a, ba, h⟩ := zorn_le_nonempty₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)

Result:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun x => x ∈ Iio k) a
⊢ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∀ c ⊆ Iio k, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ Iio k, ∀ z ∈ c, z ≤ ub

Proof state:
case eq_top_or_exists_le_coatom.mk.inl
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
left

Result:
case eq_top_or_exists_le_coatom.mk.inl.h
α : Type u_2
inst✝ : CompleteLattice α
b : α
h : IsCompactElement b
hbk : b ∈ Iic b
⊢ ⟨b, hbk⟩ = ⊤

Proof state:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2.refl
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
c : ↑(Iic k)
c₀ : ¬c = ⊤
ba : b ≤ ↑c
h : Maximal (fun x => x ∈ Iio k) ↑c
hck : ⟨↑c, ⋯⟩ < c
⊢ False

Tactic:
exact lt_irrefl _ hck

Result:
no goals

Proof state:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun x => x ∈ Iio k) a
c : ↑(Iic k)
hck : ⟨a, ⋯⟩ < c
c₀ : ¬c = ⊤
⊢ False

Tactic:
cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le

Result:
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2.refl
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
c : ↑(Iic k)
c₀ : ¬c = ⊤
ba : b ≤ ↑c
h : Maximal (fun x => x ∈ Iio k) ↑c
hck : ⟨↑c, ⋯⟩ < c
⊢ False