awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
n : ℕ
hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
h' : LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)
apply : LE.le (α := α) ((a : (a : ℕ) → α) (n + 1) : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
⊢ LT.lt (α := α) ((a : (a : ℕ) → α) (n + 1) : α) ((a : (a : ℕ) → α) (n + 1) : α)

Tactic:
apply lt_of_le_of_lt _ h'

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
n : ℕ
hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
h' : LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)
h₁ : Membership.mem (α := α) (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) ((a : (a : ℕ) → α) (n + 1) : α)
⊢ LE.le (α := α) ((a : (a : ℕ) → α) (n + 1) : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)

Tactic:
apply le_sSup

Premises used: le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
this : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
n : ℕ
hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
h' : LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)
⊢ Membership.mem (α := α) (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) ((a : (a : ℕ) → α) (n + 1) : α)

Tactic:
apply Set.mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
suffices : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
⊢ False

Tactic:
suffices sSup (Set.range a) ∈ Set.range a by
      obtain ⟨n, hn⟩ := Set.mem_range.mp this
      have h' : sSup (Set.range a) < a (n + 1) := by
        change _ > _
        simp [← hn, a.map_rel_iff]
      apply lt_irrefl (a (n + 1))
      apply lt_of_le_of_lt _ h'
      apply le_sSup
      apply Set.mem_range_self
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
x : Set.Nonempty (α := α) (range (ι := ℕ) (⇑a : (a : ℕ) → α))
a₁ : SupClosed (α := α) (range (ι := ℕ) (⇑a : (a : ℕ) → α))
⊢ Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))

Tactic:
apply h (Set.range a)

Premises used: Set.range, DFunLike.coe
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
h₁ : Membership.mem (α := α) (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) ((a : (a : ℕ) → α) 37 : α)
⊢ Set.Nonempty (α := α) (range (ι := ℕ) (⇑a : (a : ℕ) → α))

Tactic:
use a 37

Premises used: OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
⊢ Membership.mem (α := α) (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) ((a : (a : ℕ) → α) 37 : α)

Tactic:
apply Set.mem_range_self

Premises used: Set.mem_range_self
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
x : α
m : ℕ
hm : (a : (a : ℕ) → α) m = x
y : α
n : ℕ
hn : (a : (a : ℕ) → α) n = y
h₁ : (a : (a : ℕ) → α) (max m n) = x ⊔ y
⊢ Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (x ⊔ y)

Tactic:
use m ⊔ n
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
x : α
m : ℕ
hm : (a : (a : ℕ) → α) m = x
y : α
n : ℕ
hn : (a : (a : ℕ) → α) n = y
h₁ : Eq (α := α) ((a : (a : ℕ) → α) (max m n) : α) ((a : (a : ℕ) → α) m ⊔ (a : (a : ℕ) → α) n : α)
⊢ (a : (a : ℕ) → α) (max m n) = x ⊔ y

Tactic:
rw [← hm, ← hn]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
x : α
m : ℕ
hm : (a : (a : ℕ) → α) m = x
y : α
n : ℕ
hn : (a : (a : ℕ) → α) n = y
⊢ Eq (α := α) ((a : (a : ℕ) → α) (max m n) : α) ((a : (a : ℕ) → α) m ⊔ (a : (a : ℕ) → α) n : α)

Tactic:
apply RelHomClass.map_sup a

Premises used: RelHomClass.map_sup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
simp_rw : IsSupFiniteCompact α ↔ ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

Tactic:
simp_rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]

Premises used: CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
⟨fun h k s hs => ?_, fun h s => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
refine_1 :
  ∀ (h : IsSupFiniteCompact α) (k : α) (s : Set α) (hs : k ≤ sSup s), ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
refine_2 :
  ∀ (h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) (s : Set α),
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
⊢ IsSupFiniteCompact α ↔ ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
refine ⟨fun h k s hs => ?_, fun h s => ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
refine_1 :
  ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s) (htsup : sSup s = t.sup id),
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s = t.sup id
right : k ≤ t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
use t, hts
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s = t.sup id
right right₁ right₂ right₃ : k ≤ sSup s
⊢ k ≤ t.sup id

Tactic:
rwa [← htsup]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
⊢ sSup s ≤ sSup s

Tactic:
rfl
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
refine_2 :
  ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s) (htsup : sSup s ≤ t.sup id),
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id

Tactic:
obtain ⟨t, ⟨hts, htsup⟩⟩ := h (sSup s) s (by rfl)

Premises used: SupSet.sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
a : sSup s ≤ t.sup id
a₁ : t.sup id ≤ sSup s
⊢ sSup s = t.sup id

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ sSup s ≤ t.sup id

Tactic:
assumption
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
this : t.sup id ≤ sSup s
⊢ t.sup id ≤ sSup s

Tactic:
assumption
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
suffices : t.sup id ≤ sSup s
⊢ sSup s = t.sup id

Tactic:
suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
simp : ∀ b ∈ t, b ≤ sSup s
⊢ t.sup id ≤ sSup s

Tactic:
simp only [id, Finset.sup_le_iff]

Premises used: id, Finset.sup_le_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
x : α
hx : x ∈ t
⊢ x ≤ sSup s

Tactic:
le_sSup (hts hx)

Premises used: le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
x : α
hx : x ∈ t
⊢ x ≤ sSup s

Tactic:
exact le_sSup (hts hx)

Premises used: le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
⊢ sSup s = t.sup id

Tactic:
have : sSup s = t.sup id := by
      suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
      simp only [id, Finset.sup_le_iff]
      intro x hx
      exact le_sSup (hts hx)
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
this : sSup s = t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id

Tactic:
⟨t, hts, this⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
h : ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
t : Finset α
hts : (↑t : Set α) ⊆ s
htsup : sSup s ≤ t.sup id
this : sSup s = t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id

Tactic:
exact ⟨t, hts, this⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ WellFoundedGT α

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ IsSupFiniteCompact α

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ ∀ (a : WellFoundedGT α), IsSupFiniteCompact α

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ ∀ (a : WellFoundedGT α), IsSupFiniteCompact α

Tactic:
tfae_have 1 → 2 := @WellFoundedGT.isSupFiniteCompact α _

Premises used: CompleteLattice.WellFoundedGT.isSupFiniteCompact
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
⊢ IsSupFiniteCompact α

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
⊢ IsSupClosedCompact α

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
⊢ ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
⊢ ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α

Tactic:
tfae_have 2 → 3 := IsSupFiniteCompact.isSupClosedCompact α

Premises used: CompleteLattice.IsSupFiniteCompact.isSupClosedCompact
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
tfae_2_to_3 : ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α
⊢ IsSupClosedCompact α

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
tfae_2_to_3 : ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α
⊢ WellFoundedGT α

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
tfae_2_to_3 : ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α
⊢ ∀ (a : IsSupClosedCompact α), WellFoundedGT α

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
tfae_2_to_3 : ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α
⊢ ∀ (a : IsSupClosedCompact α), WellFoundedGT α

Tactic:
tfae_have 3 → 1 := IsSupClosedCompact.wellFoundedGT α

Premises used: CompleteLattice.IsSupClosedCompact.wellFoundedGT
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 α
⊢ IsSupFiniteCompact α

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 α
⊢ ∀ (k : α), IsCompactElement k

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

Tactic:
2 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k

Tactic:
tfae_have 2 ↔ 4 := isSupFiniteCompact_iff_all_elements_compact α

Premises used: CompleteLattice.isSupFiniteCompact_iff_all_elements_compact
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 α
tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ WellFoundedGT α ↔ IsSupFiniteCompact α

Tactic:
(wellFoundedGT_characterisations α).out 0 1

Premises used: List.TFAE.out, CompleteLattice.wellFoundedGT_characterisations, OfNat.ofNat
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ IsSupFiniteCompact α ↔ IsSupClosedCompact α

Tactic:
(wellFoundedGT_characterisations α).out 1 2

Premises used: List.TFAE.out, CompleteLattice.wellFoundedGT_characterisations, OfNat.ofNat
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ IsSupClosedCompact α ↔ WellFoundedGT α

Tactic:
(wellFoundedGT_characterisations α).out 2 0

Premises used: List.TFAE.out, CompleteLattice.wellFoundedGT_characterisations, OfNat.ofNat
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
by_contra! : ∀ (contra : s.Infinite), False
⊢ s.Finite

Tactic:
by_contra! contra
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
hs : sSupIndep s
contra : s.Infinite
obtain : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), False
⊢ False

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

Premises used: CompleteLattice.WellFoundedGT.isSupFiniteCompact
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
⊢ (s \ (↑(insert ⊥ t) : Set α)).Infinite

Tactic:
have : (s \ (insert ⊥ t : Finset α)).Infinite := contra.diff (Finset.finite_toSet _)
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
obtain : ∀ (x : α) (hx₁ : x ∈ s) (hx₂ : x ∉ (↑(insert ⊥ t) : Set α)), ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

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

Premises used: Set.Infinite.nonempty
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 : α
hx₁ : x ∈ s
hx₂ : x ∉ (↑(insert ⊥ t) : Set α)
⊢ x ≠ ⊥ ∧ x ∉ t

Tactic:
simpa [not_or] using hx₂

Premises used: not_or
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 : α
hx₁ : x ∈ s
hx₂ : x ∉ (↑(insert ⊥ t) : Set α)
⊢ ∃ x ∈ s, x ≠ ⊥ ∧ x ∉ t

Tactic:
exact ⟨x, hx₁, by simpa [not_or] using hx₂⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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

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₂⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
obtain : ∀ (x : α) (hx₀ : x ∈ s) (hx₁ : x ≠ ⊥) (hx₂ : x ∉ t), False
⊢ False

Tactic:
obtain ⟨x, hx₀, hx₁, hx₂⟩ := contra
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
⊢ (↑t : Set α) ∪ {x} ≤ s

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

Premises used: Set.union_singleton
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 ∈ (↑t : Set α) ∪ {x}

Tactic:
simp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
⊢ Disjoint x (sSup (((↑t : Set α) ∪ {x}) \ {x}))

Tactic:
have := hs.mono (by simp [ht₁, hx₀, -Set.union_singleton] : ↑t ∪ {x} ≤ s) (by simp : x ∈ _)
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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
this : Disjoint x (sSup (((↑t : Set α) ∪ {x}) \ {x}))
⊢ x ⊓ sSup s = ⊥

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

Premises used: Disjoint, Finset.sup_id_eq_sSup, Disjoint.eq_bot
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 = ⊥

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
-- Module: Mathlib.Order.CompactlyGenerated.Basic
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 = ⊥
apply : x = ⊥
⊢ False

Tactic:
apply hx₁