ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
let S := { x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x }
case intro.intro.intro.intro
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := h.has_min S ⟨⊥, ∅, by simp⟩
case intro.intro.intro.intro.refine'_1
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup t id

case intro.intro.intro.intro.refine'_2
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ Finset.sup t id ≤ sSup s
case intro.intro.intro.intro
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ sSup s = Finset.sup t id
refine' ⟨t, ht₁, (sSup_le _ _ fun y hy => _).antisymm _⟩
no goals
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
⊢ ↑∅ ⊆ s ∧ Finset.sup ∅ id = ⊥
simp
no goals
case intro.intro.intro.intro.refine'_1
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup t id
classical
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
    (hm _ ⟨insert y t, by simp [Set.insert_subset, hy, ht₁]⟩)]
simp
case intro.intro.intro.intro.refine'_1
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup (insert y t) id
case intro.intro.intro.intro.refine'_1
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup t id
rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
    (hm _ ⟨insert y t, by simp [Set.insert_subset, hy, ht₁]⟩)]
no goals
case intro.intro.intro.intro.refine'_1
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ y ≤ Finset.sup (insert y t) id
simp
no goals
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
y : α
hy : y ∈ s
⊢ ↑(insert y t) ⊆ s ∧ Finset.sup (insert y t) id = Finset.sup (insert y t) id
simp [Set.insert_subset, hy, ht₁]
case intro.intro.intro.intro.refine'_2
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ sSup ↑t ≤ sSup s
case intro.intro.intro.intro.refine'_2
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ Finset.sup t id ≤ sSup s
rw [Finset.sup_id_eq_sSup]
no goals
case intro.intro.intro.intro.refine'_2
ι : Sort ?u.16216
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ Finset.sup t id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ (x : α), x ∈ S → ¬x > Finset.sup t id
⊢ sSup ↑t ≤ sSup s
exact sSup_le_sSup ht₁