awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
simp_rw simp_rw₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup f ≤ x
simp_rw₂ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup (id ∘ f) ≤ x
simp_rw₃ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, (Finset.image f s).sup id ≤ x
a a₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (x : α)
    (hx : x ∈ Finset.image f s), ∃ y ∈ d, x ≤ y
⊢ IsCompactElement (s.sup f)
have a₂ : ∀
  (h :
    ∀ x ∈ s, ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
  (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
  (hps : p ∈ s) (hx : f p ∈ Finset.image f s), ∃ y ∈ d, f p ≤ y
Tactic: classical
    simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h
    intro d hemp hdir hsup
    rw [← Function.id_comp f]
    rw [← Finset.sup_image]
    apply Finset.sup_le_of_le_directed d hemp hdir
    rintro x hx
    obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
    specialize h p hps
    specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
    simpa only [exists_prop]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
simp_rw simp_rw₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup f ≤ x
simp_rw₂ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup (id ∘ f) ≤ x
simp_rw₃ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, (Finset.image f s).sup id ≤ x
a a₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (x : α)
    (hx : x ∈ Finset.image f s), ∃ y ∈ d, x ≤ y
a₂ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
    (hps : p ∈ s) (hx : f p ∈ Finset.image f s), ∃ y ∈ d, f p ≤ y
⊢ IsCompactElement (s.sup f)
have a₃ : ∀ (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
  (hps : p ∈ s) (hx : f p ∈ Finset.image f s)
  (h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f p ≤ sSup s → ∃ x ∈ s, f p ≤ x),
  ∃ y ∈ d, f p ≤ y
Tactic: classical
    simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h
    intro d hemp hdir hsup
    rw [← Function.id_comp f]
    rw [← Finset.sup_image]
    apply Finset.sup_le_of_le_directed d hemp hdir
    rintro x hx
    obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
    specialize h p hps
    specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
    simpa only [exists_prop]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
inst : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
simp_rw simp_rw₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup f ≤ x
simp_rw₂ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, s.sup (id ∘ f) ≤ x
simp_rw₃ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d),
    ∃ x ∈ d, (Finset.image f s).sup id ≤ x
a a₁ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (x : α)
    (hx : x ∈ Finset.image f s), ∃ y ∈ d, x ≤ y
a₂ :
  ∀
    (h :
      ∀ x ∈ s,
        ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f x ≤ sSup s → ∃ x_1 ∈ s, f x ≤ x_1)
    (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
    (hps : p ∈ s) (hx : f p ∈ Finset.image f s), ∃ y ∈ d, f p ≤ y
a₃ :
  ∀ (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
    (hps : p ∈ s) (hx : f p ∈ Finset.image f s)
    (h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → f p ≤ sSup s → ∃ x ∈ s, f p ≤ x),
    ∃ y ∈ d, f p ≤ y
⊢ IsCompactElement (s.sup f)
have a₄ : ∀ (d : Set α) (hemp : d.Nonempty) (hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (hsup : s.sup f ≤ sSup d) (p : β)
  (hps : p ∈ s) (hx : f p ∈ Finset.image f s) (h : ∃ x ∈ d, f p ≤ x), ∃ y ∈ d, f p ≤ y
Tactic: classical
    simp_rw [isCompactElement_iff_le_of_directed_sSup_le] at ⊢ h
    intro d hemp hdir hsup
    rw [← Function.id_comp f]
    rw [← Finset.sup_image]
    apply Finset.sup_le_of_le_directed d hemp hdir
    rintro x hx
    obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
    specialize h p hps
    specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
    simpa only [exists_prop]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
have obtain : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (hm : ∀ x ∈ S, ¬t.sup id < x),
  ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
Tactic: obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
have refine_1 : ∀ (y : α) (hy : y ∈ s), y ≤ t.sup id
Tactic: refine ⟨t, ht₁, (sSup_le fun y hy => ?_).antisymm ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
refine_1 : ∀ (y : α) (hy : y ∈ s), y ≤ t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
have refine_2 : t.sup id ≤ sSup s
Tactic: refine ⟨t, ht₁, (sSup_le fun y hy => ?_).antisymm ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ t.sup id
have refine_1 : y ≤ (insert y t).sup id
Tactic: rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
y : α
hy : y ∈ s
⊢ y ≤ t.sup id
have refine_1 : y ≤ (insert y t).sup id
Tactic: classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
inst_1 : WellFoundedGT α
s : Set α
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ t.sup id ≤ sSup s
have refine_2 : sSup (↑t : Set α) ≤ sSup s
Tactic: rw [Finset.sup_id_eq_sSup]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupFiniteCompact α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
⊢ sSup s ∈ s
have obtain : ∀ (t : Finset α) (ht₁ : (↑t : Set α) ⊆ s) (ht₂ : sSup s = t.sup id), sSup s ∈ s
Tactic: obtain ⟨t, ht₁, ht₂⟩ := h s
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
⊢ sSup s ∈ s
have inl : ∀ (ht₁ : (↑∅ : Set α) ⊆ s) (ht₂ : sSup s = Finset.sup ∅ id), sSup s ∈ s
Tactic: rcases t.eq_empty_or_nonempty with rfl | h
Cleared hypotheses: t, ht₁, ht₂
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
inl : ∀ (ht₁ : (↑∅ : Set α) ⊆ s) (ht₂ : sSup s = Finset.sup ∅ id), sSup s ∈ s
⊢ sSup s ∈ s
have inr : ∀ (h : t.Nonempty), sSup s ∈ s
Tactic: rcases t.eq_empty_or_nonempty with rfl | h
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : (↑∅ : Set α) ⊆ s
ht₂ : sSup s = Finset.sup ∅ id
⊢ sSup s ∈ s
have ht₃ : sSup s = ⊥
Tactic: rw [Finset.sup_empty] at ht₂
Cleared hypotheses: ht₂
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
ht₁ : (↑∅ : Set α) ⊆ s
ht₂ : sSup s = ⊥
⊢ sSup s ∈ s
have inl : ⊥ ∈ s
Tactic: rw [ht₂]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
s : Set α
hne : s.Nonempty
hsc : SupClosed s
t : Finset α
ht₁ : (↑t : Set α) ⊆ s
ht₂ : sSup s = t.sup id
h : t.Nonempty
⊢ sSup s ∈ s
have inr : t.sup id ∈ s
Tactic: rw [ht₂]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
⊢ WellFounded fun (x1 x2 : α) ↦ x2 < x1
have refine : ∀ (a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1), False
Tactic: refine RelEmbedding.wellFounded_iff_isEmpty.mpr ⟨fun a => ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : ℕ) → α)))
⊢ False
have obtain : ∀ (n : ℕ) (hn : Eq (α := α) ((a : (a : ℕ) → α) n : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)), False
Tactic: obtain ⟨n, hn⟩ := Set.mem_range.mp this
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : ℕ) → α)) : α)
⊢ LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)
have change : GT.gt (α := α) ((a : (a : ℕ) → α) (n + 1) : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
Tactic: change _ > _
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 : ℕ) → α)) : α)
⊢ False
have h' : LT.lt (α := α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α) ((a : (a : ℕ) → α) (n + 1) : α)
Tactic: have h' : sSup (Set.range a) < a (n + 1) := by
        change _ > _
        simp [← hn, a.map_rel_iff]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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) : α)
⊢ False
have apply : LT.lt (α := α) ((a : (a : ℕ) → α) (n + 1) : α) ((a : (a : ℕ) → α) (n + 1) : α)
Tactic: apply lt_irrefl (a (n + 1))
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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) : α)
⊢ LT.lt (α := α) ((a : (a : ℕ) → α) (n + 1) : α) ((a : (a : ℕ) → α) (n + 1) : α)
have apply : LE.le (α := α) ((a : (a : ℕ) → α) (n + 1) : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
Tactic: apply lt_of_le_of_lt _ h'
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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) : α)
⊢ LE.le (α := α) ((a : (a : ℕ) → α) (n + 1) : α) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)) : α)
have h₁ : Membership.mem (α := α) (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) ((a : (a : ℕ) → α) (n + 1) : α)
Tactic: apply le_sSup
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
⊢ False
have suffices : Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
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
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
have x : Set.Nonempty (α := α) (range (ι := ℕ) (⇑a : (a : ℕ) → α))
Tactic: apply h (Set.range a)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : ℕ) → α))
⊢ Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (sSup (range (ι := ℕ) (⇑a : (a : ℕ) → α)))
have a₁ : SupClosed (α := α) (range (ι := ℕ) (⇑a : (a : ℕ) → α))
Tactic: apply h (Set.range a)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupClosedCompact α
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
⊢ Set.Nonempty (α := α) (range (ι := ℕ) (⇑a : (a : ℕ) → α))
have h₁ : Membership.mem (α := α) (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) ((a : (a : ℕ) → α) 37 : α)
Tactic: use a 37
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ Membership.mem (γ := Set α) (range (ι := ℕ) (⇑a : (a : ℕ) → α)) (x ⊔ y)
have h₁ : (a : (a : ℕ) → α) (max m n) = x ⊔ y
Tactic: use m ⊔ n
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ (a : (a : ℕ) → α) (max m n) = x ⊔ y
have h₁ : Eq (α := α) ((a : (a : ℕ) → α) (max m n) : α) ((a : (a : ℕ) → α) m ⊔ (a : (a : ℕ) → α) n : α)
Tactic: rw [← hm, ← hn]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
have simp_rw : IsSupFiniteCompact α ↔ ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: simp_rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ IsSupFiniteCompact α ↔ ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have refine_1 : ∀ (h : IsSupFiniteCompact α) (k : α) (s : Set α) (hs : k ≤ sSup s), ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: refine ⟨fun h k s hs => ?_, fun h s => ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ IsSupFiniteCompact α ↔ ∀ (k : α) (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have 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
Tactic: refine ⟨fun h k s hs => ?_, fun h s => ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
h : IsSupFiniteCompact α
k : α
s : Set α
hs : k ≤ sSup s
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have refine_1 : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s) (htsup : sSup s = t.sup id), ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: obtain ⟨t, ⟨hts, htsup⟩⟩ := h s
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have right : k ≤ t.sup id
Tactic: use t, hts
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
have refine_2 : ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s) (htsup : 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)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have suffices : t.sup id ≤ sSup s
Tactic: suffices t.sup id ≤ sSup s by apply le_antisymm <;> assumption
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ t.sup id ≤ sSup s
have simp : ∀ b ∈ t, b ≤ sSup s
Tactic: simp only [id, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ sSup s = t.sup id
have this : 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)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE
have tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
Tactic: tfae_have 1 → 2 := @WellFoundedGT.isSupFiniteCompact α _
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
Goal:
α : Type u_2
inst : CompleteLattice α
tfae_1_to_2 : ∀ (a : WellFoundedGT α), IsSupFiniteCompact α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE
have tfae_2_to_3 : ∀ (a : IsSupFiniteCompact α), IsSupClosedCompact α
Tactic: tfae_have 2 → 3 := IsSupFiniteCompact.isSupClosedCompact α