case eq_top_or_exists_le_coatom
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
⊢ ∀ (b : ↑(Set.Iic k)), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
⊢ IsCoatomic ↑(Set.Iic k)
constructor
case eq_top_or_exists_le_coatom.mk
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
case eq_top_or_exists_le_coatom
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
⊢ ∀ (b : ↑(Set.Iic k)), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
rintro ⟨b, hbk⟩
case eq_top_or_exists_le_coatom.mk.inl
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a

case eq_top_or_exists_le_coatom.mk.inr
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
case eq_top_or_exists_le_coatom.mk
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
obtain rfl | H := eq_or_ne b k
case eq_top_or_exists_le_coatom.mk.inr.h
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
case eq_top_or_exists_le_coatom.mk.inr
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
right
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih : ?eq_top_or_exists_le_coatom.mk.inr.h.refine_1
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a

case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ Sort ?u.111663

case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ?eq_top_or_exists_le_coatom.mk.inr.h.refine_1
case eq_top_or_exists_le_coatom.mk.inr.h
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
have ih : ?_ := ?_
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3.intro.intro.intro
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih : ?eq_top_or_exists_le_coatom.mk.inr.h.refine_1
a : α
a₀ : a ∈ Set.Iio k
ba : b ≤ a
h : ∀ (z : α), z ∈ Set.Iio k → a ≤ z → z = a
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a

case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ Sort ?u.111663

case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ?eq_top_or_exists_le_coatom.mk.inr.h.refine_1
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih : ?eq_top_or_exists_le_coatom.mk.inr.h.refine_1
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a

case eq_top_or_exists_le_coatom.mk.inr.h.refine_1
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ Sort ?u.111663

case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ?eq_top_or_exists_le_coatom.mk.inr.h.refine_1
obtain ⟨a, a₀, ba, h⟩ := zorn_nonempty_partialOrder₀ (Set.Iio k) ih b (lt_of_le_of_ne hbk H)
case eq_top_or_exists_le_coatom.mk.inl.h
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ { val := b, property := hbk } = ⊤
case eq_top_or_exists_le_coatom.mk.inl
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ { val := b, property := hbk } = ⊤ ∨ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
left
case eq_top_or_exists_le_coatom.mk.inl.h.a
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ ↑{ val := b, property := hbk } = ↑⊤
case eq_top_or_exists_le_coatom.mk.inl.h
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ { val := b, property := hbk } = ⊤
ext
no goals
case eq_top_or_exists_le_coatom.mk.inl.h.a
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
b : α
h : IsCompactElement b
hbk : b ∈ Set.Iic b
⊢ ↑{ val := b, property := hbk } = ↑⊤
simp only [Set.Iic.coe_top, Subtype.coe_mk]
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3.intro.intro.intro
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih :
  ∀ (c : Set α),
    c ⊆ Set.Iio k →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ c → z ≤ ub
a : α
a₀ : a ∈ Set.Iio k
ba : b ≤ a
h : ∀ (z : α), z ∈ Set.Iio k → a ≤ z → z = a
c : ↑(Set.Iic k)
hck : { val := a, property := (_ : a ≤ k) } < c
c₀ : ¬c = ⊤
⊢ False
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3.intro.intro.intro
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih : ?eq_top_or_exists_le_coatom.mk.inr.h.refine_1
a : α
a₀ : a ∈ Set.Iio k
ba : b ≤ a
h : ∀ (z : α), z ∈ Set.Iio k → a ≤ z → z = a
⊢ ∃ a, IsCoatom a ∧ { val := b, property := hbk } ≤ a
refine' ⟨⟨a, le_of_lt a₀⟩, ⟨ne_of_lt a₀, fun c hck => by_contradiction fun c₀ => _⟩, ba⟩
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3.intro.intro.intro.refl
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih :
  ∀ (c : Set α),
    c ⊆ Set.Iio k →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ c → z ≤ ub
c : ↑(Set.Iic k)
c₀ : ¬c = ⊤
a₀ : ↑c ∈ Set.Iio k
ba : b ≤ ↑c
h : ∀ (z : α), z ∈ Set.Iio k → ↑c ≤ z → z = ↑c
hck : { val := ↑c, property := (_ : ↑c ≤ k) } < c
⊢ False
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3.intro.intro.intro
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih :
  ∀ (c : Set α),
    c ⊆ Set.Iio k →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ c → z ≤ ub
a : α
a₀ : a ∈ Set.Iio k
ba : b ≤ a
h : ∀ (z : α), z ∈ Set.Iio k → a ≤ z → z = a
c : ↑(Set.Iic k)
hck : { val := a, property := (_ : a ≤ k) } < c
c₀ : ¬c = ⊤
⊢ False
cases h c.1 (lt_of_le_of_ne c.2 fun con => c₀ (Subtype.ext con)) hck.le
no goals
case eq_top_or_exists_le_coatom.mk.inr.h.refine_3.intro.intro.intro.refl
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
ih :
  ∀ (c : Set α),
    c ⊆ Set.Iio k →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ c → z ≤ ub
c : ↑(Set.Iic k)
c₀ : ¬c = ⊤
a₀ : ↑c ∈ Set.Iio k
ba : b ≤ ↑c
h : ∀ (z : α), z ∈ Set.Iio k → ↑c ≤ z → z = ↑c
hck : { val := ↑c, property := (_ : ↑c ≤ k) } < c
⊢ False
exact lt_irrefl _ hck
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
⊢ ∀ (c : Set α),
    c ⊆ Set.Iio k →
      IsChain (fun x x_1 => x ≤ x_1) c → ∀ (y : α), y ∈ c → ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ c → z ≤ ub
intro S SC cC I _
case pos
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub

case neg
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : ¬Set.Nonempty S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
case eq_top_or_exists_le_coatom.mk.inr.h.refine_2
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
by_cases hS : S.Nonempty
no goals
case neg
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : ¬Set.Nonempty S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
exact
  ⟨b, lt_of_le_of_ne hbk H, by
    simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
      forall_prop_of_false, not_false_iff]⟩
case pos
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
⊢ ∀ (z : α), z ∈ S → z ≤ sSup S
case pos
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
⊢ ∃ ub, ub ∈ Set.Iio k ∧ ∀ (z : α), z ∈ S → z ≤ ub
refine' ⟨sSup S, h.directed_sSup_lt_of_lt hS cC.directedOn SC, _⟩
case pos
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S
case pos
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
⊢ ∀ (z : α), z ∈ S → z ≤ sSup S
intro
no goals
case pos
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : Set.Nonempty S
z✝ : α
⊢ z✝ ∈ S → z✝ ≤ sSup S
apply le_sSup
no goals
ι : Sort ?u.110031
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Set.Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Set.Iio k
cC : IsChain (fun x x_1 => x ≤ x_1) S
I : α
a✝ : I ∈ S
hS : ¬Set.Nonempty S
⊢ ∀ (z : α), z ∈ S → z ≤ b
simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
  forall_prop_of_false, not_false_iff]