ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
⊢ False
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
⊢ Set.Finite s
refine' Set.not_infinite.mp fun contra => _
case intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ False
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
⊢ False
obtain ⟨t, ht₁, ht₂⟩ := WellFounded.isSupFiniteCompact α h s
case contra
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t

case intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
contra : ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
⊢ False
case intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ False
replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t
case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ False
case intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
contra : ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
⊢ False
obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
case hs
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ x ⊓ sSup s = ⊥

case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ False
case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ False
replace hs : x ⊓ sSup s = ⊥
case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥
case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ False
apply hx₁
case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s
case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥
rw [← hs, eq_comm, inf_eq_left]
no goals
case intro.intro.intro.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s
exact le_sSup _ _ hx₀
case contra
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
case contra
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
case contra.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
x : α
hx₁ : x ∈ s
hx₂ : ¬x ∈ ↑(insert ⊥ t)
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
case contra
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
no goals
case contra.intro.intro
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
x : α
hx₁ : x ∈ s
hx₂ : ¬x ∈ ↑(insert ⊥ t)
⊢ ∃ x, x ∈ s ∧ x ≠ ⊥ ∧ ¬x ∈ t
exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
no goals
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
contra : Set.Infinite s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
this : Set.Infinite (s \ ↑(insert ⊥ t))
x : α
hx₁ : x ∈ s
hx₂ : ¬x ∈ ↑(insert ⊥ t)
⊢ x ≠ ⊥ ∧ ¬x ∈ t
simpa [not_or] using hx₂
case hs
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥
case hs
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ x ⊓ sSup s = ⊥
have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
no goals
case hs
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥
simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
no goals
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ ↑t ∪ {x} ≤ s
simp [ht₁, hx₀, -Set.union_singleton]
no goals
ι : Sort ?u.78582
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
h : WellFounded fun x x_1 => x > x_1
s : Set α
hs : SetIndependent s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = Finset.sup t id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : ¬x ∈ t
⊢ x ∈ ↑t ∪ {x}
simp