-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem WellFoundedGT.finite_of_sSupIndep [WellFoundedGT α] {s : Set α}
    (hs : sSupIndep s) : s.Finite

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ x ∈ ↑t ∪ {x}

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥

Tactic:
rw [← hs, eq_comm, inf_eq_left]

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
x : α
hx₁ : x ∈ s
hx₂ : x ∉ ↑(insert ⊥ t)
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

Tactic:
exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

Tactic:
have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := this.nonempty

Result:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
x : α
hx₁ : x ∈ s
hx₂ : x ∉ ↑(insert ⊥ t)
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ False

Tactic:
apply hx₁

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ False

Tactic:
replace hs : x ⊓ sSup s = ⊥ := by
  have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
  simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ False

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
⊢ False

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s

Result:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
⊢ False

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
⊢ s.Finite

Tactic:
refine Set.not_infinite.mp fun contra => ?_

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
⊢ False

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥

Tactic:
simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
⊢ s.Finite

Tactic:
classical
  refine Set.not_infinite.mp fun contra => ?_
  obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s
  replace contra : ∃ x : α, x ∈ s ∧ x ≠ ⊥ ∧ x ∉ t := by
    have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
    obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
    exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
  obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
  replace hs : x ⊓ sSup s = ⊥ := by
    have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
    simpa [Disjoint, hx₂, ← t.sup_id_eq_sSup, ← ht₂] using this.eq_bot
  apply hx₁
  rw [← hs, eq_comm, inf_eq_left]
  exact le_sSup hx₀

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ ↑(insert ⊥ t)).Infinite
x : α
hx₁ : x ∈ s
hx₂ : x ∉ ↑(insert ⊥ t)
⊢ x ≠ ⊥ ∧ x ∉ t

Tactic:
simpa [not_or] using hx₂

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ ↑t ∪ {x} ≤ s

Tactic:
simp [ht₁, hx₀, -Set.union_singleton]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ x ⊓ sSup s = ⊥

Tactic:
have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
this : Disjoint x (sSup ((↑t ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x ≤ sSup s

Tactic:
exact le_sSup hx₀

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
⊢ False

Tactic:
obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : ↑t ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ False