awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
tfae_2_to_3 : ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE
have tfae_3_to_1 : ∀ (a : IsSupClosedCompact α), WellFoundedGT α
Tactic: tfae_have 3 → 1 := IsSupClosedCompact.wellFoundedGT α
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
tfae_2_to_3 : ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α
tfae_3_to_1 : ∀ (a : IsSupClosedCompact α), WellFoundedGT α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE
have tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
Tactic: tfae_have 2 ↔ 4 := isSupFiniteCompact_iff_all_elements_compact α
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
⊢ s.Finite
have by_contra! : ∀ (contra : s.Infinite), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
⊢ False
have obtain : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
Tactic: obtain ⟨t, ht₁, ht₂⟩ := CompleteLattice.WellFoundedGT.isSupFiniteCompact α s
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
have this : (s \ (↑(insert ⊥ t) : Set α)).Infinite
Tactic: have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
this : (s \ (↑(insert ⊥ t) : Set α)).Infinite
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
have obtain : ∀ (x : α) (hx₁ : x ∈ s) (hx₂ : x ∉ (↑(insert ⊥ t) : Set α)), ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
Tactic: obtain ⟨x, hx₁, hx₂⟩ := this.nonempty
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
⊢ False
have contra₁ : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
Tactic: 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₂⟩
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
⊢ False
have obtain : ∀ (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t), False
Tactic: obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ x ⊓ sSup s = ⊥
have this : Disjoint x (sSup (((↑t : Set α) ∪ {x}) \ {x}))
Tactic: have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
⊢ False
have hs₁ : x ⊓ sSup s = ⊥
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ False
have apply : x = ⊥
Tactic: apply hx₁
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
x : α
hx₀ : x ∈ s
hx₁ : x ≠ ⊥
hx₂ : x ∉ t
hs : x ⊓ sSup s = ⊥
⊢ x = ⊥
have rw : x ≤ sSup s
Tactic: rw [← hs, eq_comm, inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
⊢ s.Finite
have by_contra! : ¬s.Finite → False
Tactic: classical
    by_contra! 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₀
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
⊢ s.Finite
have by_contra!₄ : s.Infinite → False
Tactic: classical
    by_contra! 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₀
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (contra : s.Infinite), False
⊢ s.Finite
have by_contra!₁₁ : ∀ (contra : s.Infinite) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
Tactic: classical
    by_contra! 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₀
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (contra : s.Infinite), False
by_contra!₁₁ : ∀ (contra : s.Infinite) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
⊢ s.Finite
have by_contra!₁₂ : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t), False
Tactic: classical
    by_contra! 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₀
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (contra : s.Infinite), False
by_contra!₁₁ : ∀ (contra : s.Infinite) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
by_contra!₁₂ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t), False
⊢ s.Finite
have by_contra!₁₃ : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t),
  False
Tactic: classical
    by_contra! 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₀
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (contra : s.Infinite), False
by_contra!₁₁ : ∀ (contra : s.Infinite) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
by_contra!₁₂ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t), False
by_contra!₁₃ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t),
    False
⊢ s.Finite
have by_contra!₁₄ : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
  (hs : x ⊓ sSup s = ⊥), False
Tactic: classical
    by_contra! 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₀
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (contra : s.Infinite), False
by_contra!₁₁ : ∀ (contra : s.Infinite) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
by_contra!₁₂ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t), False
by_contra!₁₃ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t),
    False
by_contra!₁₄ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
    (hs : x ⊓ sSup s = ⊥), False
⊢ s.Finite
have by_contra!₁₅ : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
  (hs : x ⊓ sSup s = ⊥), x = ⊥
Tactic: classical
    by_contra! 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₀
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : ¬s.Finite → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ : ∀ (contra : s.Infinite), False
by_contra!₁₁ : ∀ (contra : s.Infinite) (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
by_contra!₁₂ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (contra : ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t), False
by_contra!₁₃ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t),
    False
by_contra!₁₄ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
    (hs : x ⊓ sSup s = ⊥), False
by_contra!₁₅ :
  ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
    (hs : x ⊓ sSup s = ⊥), x = ⊥
⊢ s.Finite
have by_contra!₁₆ : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id) (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t)
  (hs : x ⊓ sSup s = ⊥), x ≤ sSup s
Tactic: classical
    by_contra! 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₀
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ Set.Finite.{u_3} (α := ι) {i : ι | t i ≠ ⊥}
have refine : (range t).Finite
Tactic: refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
⊢ s.Finite
have by_contra : ∀ (inf : ¬s.Finite), False
Tactic: by_contra inf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
⊢ False
have sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
Tactic: have sup_le n : (e n).1 ⊔ a (n + 1) ≤ a n := sup_le_iff.mpr ⟨le_iSup₂_of_le n le_rfl le_rfl,
    iSup₂_le fun i hi ↦ le_iSup₂_of_le i (n.le_succ.trans hi) le_rfl⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
⊢ False
have refine_2 : ∀ (lt : ∀ (n : ℕ), a (n + 1) < a n), False
Tactic: have lt n : a (n + 1) < a n := (Disjoint.right_lt_sup_of_left_ne_bot
    ((hs (e n).2.1).mono_right <| iSup₂_le fun i hi ↦ le_sSup ?_) (e n).2.2).trans_le (sup_le n)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
s : Set α
hs : sSupIndep s
inf : ¬s.Finite
e : ℕ ↪ (↑(s \ {⊥}) : Type u_2) := Infinite.natEmbedding (↑(s \ {⊥}) : Type u_2)
a : (n : ℕ) → α := fun (n : ℕ) ↦ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α)
sup_le : ∀ (n : ℕ), (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α) ⊔ a (n + 1) ≤ a n
refine_2 : ∀ (lt : ∀ (n : ℕ), a (n + 1) < a n), False
⊢ False
have refine_1 : ∀ (n i : ℕ) (hi : i ≥ n + 1),
  (↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) i) : α) ∈ s \ {(↑((e : (a : ℕ) → (↑(s \ {⊥}) : Type u_2)) n) : α)}
Tactic: have lt n : a (n + 1) < a n := (Disjoint.right_lt_sup_of_left_ne_bot
    ((hs (e n).2.1).mono_right <| iSup₂_le fun i hi ↦ le_sSup ?_) (e n).2.2).trans_le (sup_le n)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedLT α
ι : Type u_3
t : ι → α
ht : iSupIndep t
⊢ Set.Finite.{u_3} (α := ι) {i : ι | t i ≠ ⊥}
have refine : (range t).Finite
Tactic: refine Finite.of_finite_image (Finite.subset ?_ (image_subset_range t _)) ht.injOn
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
b : α
⊢ sSup {c : α | IsCompactElement c ∧ c ≤ b} = b
have rcases : ∀ (s : Set α) (hs : ∀ x ∈ s, IsCompactElement x), sSup {c : α | IsCompactElement c ∧ c ≤ sSup s} = sSup s
Tactic: rcases IsCompactlyGenerated.exists_sSup_eq b with ⟨s, hs, rfl⟩
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) ⊤
have rw : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) (sSup {c : α | IsCompactElement c ∧ c ≤ ⊤})
Tactic: rw [← sSup_compact_le_eq ⊤]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
⊢ Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) (sSup {c : α | IsCompactElement c ∧ c ≤ ⊤})
have simp_rw : Eq.{u_2 + 1} (α := α) (sSup {a : α | IsCompactElement a}) (sSup {c : α | IsCompactElement c ∧ True})
Tactic: simp_rw [le_top, and_true]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a b : α
h : ∀ (c : α), IsCompactElement c → c ≤ a → c ≤ b
⊢ a ≤ b
have rw : LE.le.{u_2} (α := α) (sSup {c : α | IsCompactElement c ∧ c ≤ a}) (sSup {c : α | IsCompactElement c ∧ c ≤ b})
Tactic: rw [← sSup_compact_le_eq a, ← sSup_compact_le_eq b]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
have rw : ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
Tactic: rw [le_iff_compact_le_imp]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
have pos : ∀ (hs : s.Nonempty) (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
Tactic: by_cases hs : s.Nonempty
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
pos : ∀ (hs : s.Nonempty) (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
have neg : ∀ (hs : ¬s.Nonempty) (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
Tactic: by_cases hs : s.Nonempty
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : IsCompactElement c
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b
have hc₁ : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
Tactic: rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc
Cleared hypotheses: hc, hcinf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ⊓ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b
have hcinf₁ : c ≤ a ∧ c ≤ sSup s
Tactic: rw [le_inf_iff] at hcinf
Cleared hypotheses: hcinf
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : s.Nonempty
c : α
hc : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → c ≤ sSup s → ∃ x ∈ s, c ≤ x
hcinf : c ≤ a ∧ c ≤ sSup s
⊢ c ≤ ⨆ b ∈ s, a ⊓ b
have pos : ∀ (d : α) (ds : d ∈ s) (cd : c ≤ d), c ≤ ⨆ b ∈ s, a ⊓ b
Tactic: rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hs : ¬s.Nonempty
⊢ ∀ (c : α), IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ b ∈ s, a ⊓ b
have hs₁ : s = ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty] at hs
Cleared hypotheses: hs