awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → (_ : x ∈ s) → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
⊢ cof α ≤ #(↑s : Type u_1)
have refine : ∀ (a : α), ∃ (y : α), Membership.mem (γ := Set α) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : Set α) sorry) y ∧ a ≤ y
Tactic: refine (cof_le (s := range fun x ↦ f x.1 x.2) fun a ↦ ?_).trans mk_range_le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → (_ : x ∈ s) → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
a : α
⊢ ∃ (y : α), Membership.mem (γ := Set α) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : Set α) ⋯) y ∧ a ≤ y
have obtain : ∀ (b : α) (hab : a ≤ b) (t : Set α) (ht : t ∈ s) (hb : b ∈ t),
  ∃ (y : α), Membership.mem (γ := Set α) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : Set α) sorry) y ∧ a ≤ y
Tactic: obtain ⟨b, ⟨t, ht, hb⟩, hab⟩ := h₁ a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (hypothesis)
Goal:
α ι : Type u_1
inst : LinearOrder α
s : ι → Set α
h₁ : IsCofinal.{u_1} (α := α) (⋃ (i : ι), s i)
h₂ : #ι < cof α
⊢ ∃ (i : ι), IsCofinal (s i)
have h₃ : IsCofinal (⋃₀ range s)
Tactic: rw [← sUnion_range] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Basic (goal)
Goal:
α ι : Type u_1
inst : LinearOrder α
s : ι → Set α
h₁ : IsCofinal (⋃₀ range s)
h₂ : #ι < cof α
⊢ ∃ (i : ι), IsCofinal (s i)
have obtain : ∀ (i : ι) (h : IsCofinal (s i)), ∃ (i : ι), IsCofinal (s i)
Tactic: obtain ⟨_, ⟨i, rfl⟩, h⟩ := isCofinal_of_isCofinal_sUnion h₁ (mk_range_le.trans_lt h₂)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
inst_1 : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)
have refine : IsCofinal (⋂₀ s)
Tactic: refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
inst_1 : OrderTop α
hs : ∀ x ∈ s, IsClub x
⊢ IsCofinal (⋂₀ s)
have rw : ∀ t ∈ s, ⊤ ∈ t
Tactic: rw [isCofinal_iff_top_mem, Set.mem_sInter]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)
have inl : IsEmpty α → IsClub (⋂₀ s)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
inl : IsEmpty α → IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)
have inr : Nonempty α → IsClub (⋂₀ s)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
⊢ IsClub (⋂₀ s)
have inr : ∀ (val : OrderTop α), IsClub (⋂₀ s)
Tactic: cases topOrderOrNoTopOrder α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
inr : ∀ (val : OrderTop α), IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)
have inr₁ : NoTopOrder α → IsClub (⋂₀ s)
Tactic: cases topOrderOrNoTopOrder α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)
have inl : IsEmpty α → IsClub (⋂₀ s)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
inl : IsEmpty α → IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)
have inr : Nonempty α → IsClub (⋂₀ s)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
⊢ IsClub (⋂₀ s)
have inr : ∀ (hα : cof α < ℵ₀), IsClub (⋂₀ s)
Tactic: obtain hα | hα := hα.lt_or_gt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
inr : ∀ (hα : cof α < ℵ₀), IsClub (⋂₀ s)
⊢ IsClub (⋂₀ s)
have inr₁ : ∀ (hα : ℵ₀ < cof α), IsClub (⋂₀ s)
Tactic: obtain hα | hα := hα.lt_or_gt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
⊢ IsClub (⋂₀ s)
have inr : ∀ (a : α), ∃ y ∈ ⋂₀ s, a ≤ y
Tactic: refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
⊢ ∃ y ∈ ⋂₀ s, a ≤ y
have inr : ∀ (f : (x : (↑s : Type v)) → (x : α) → α)
  (hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1), ∃ y ∈ ⋂₀ s, a ≤ y
Tactic: choose f hf using fun x : s ↦ (hs _ x.2).isCofinal
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
⊢ BddAbove (Set.range g)
have refine : ∀ (hg : IsCofinal (Set.range g)), #(↑(Set.range g) : Type v) ≤ ℵ₀
Tactic: refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (hypothesis)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
⊢ ∃ y ∈ ⋂₀ s, a ≤ y
have hg : BddAbove (Set.range g)
Tactic: have hg : BddAbove (.range g) := by
    refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)
    simpa using mk_range_le_lift (f := g)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
⊢ ∃ y ∈ ⋂₀ s, a ≤ y
have inr : ∀ (t : Set α) (ht : t ∈ s), sSup (Set.range g) ∈ t
Tactic: refine ⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
⊢ sSup (Set.range g) ∈ t
have inr : IsLUB (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) (sSup (Set.range g))
Tactic: apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (Set.range_nonempty _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
inr : IsLUB (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) (sSup (Set.range g))
⊢ sSup (Set.range g) ∈ t
have apply : (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) ⊆ t
Tactic: apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (Set.range_nonempty _)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
⊢ IsLUB (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) (sSup (Set.range g))
have inr : Membership.mem (γ := Set α)
  (upperBounds (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n))) (sSup (Set.range g))
Tactic: refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
inr :
  Membership.mem (γ := Set α)
    (upperBounds (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)))
    (sSup (Set.range g))
⊢ IsLUB (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) (sSup (Set.range g))
have inr₁ : ∀ (b : α)
  (hb :
    Membership.mem (γ := Set α)
      (upperBounds (Set.range fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n))) b),
  b ∈ upperBounds (Set.range g)
Tactic: refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ (fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n ≤ sSup (Set.range g)
have apply : ¬IsCofinal.{v} (α := α)
    (Set.range fun (x : (↑s : Type v)) ↦
      f x
        (Nat.rec (motive := fun (x : ℕ) ↦ α) a
          (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
Tactic: apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
n : ℕ
apply :
  ¬IsCofinal.{v} (α := α)
      (Set.range fun (x : (↑s : Type v)) ↦
        f x
          (Nat.rec (motive := fun (x : ℕ) ↦ α) a
            (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
⊢ (fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n ≤ sSup (Set.range g)
have apply₁ : Membership.mem (γ := Set α)
  (Set.range fun (x : (↑s : Type v)) ↦
    f x
      (Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH))
        n))
  ((fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n)
Tactic: apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ Membership.mem (γ := Set α)
    (Set.range fun (x : (↑s : Type v)) ↦
      f x
        (Nat.rec (motive := fun (x : ℕ) ↦ α) a
          (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
    ((fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n)
have w : (↑s : Type v)
Tactic: use ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set (Set α)
hα_1 : cof α ≠ ℵ₀
hsα : #(↑s : Type v) < cof α
hs : ∀ x ∈ s, IsClub x
h : Nonempty α
hα : ℵ₀ < cof α
a : α
f : (x : (↑s : Type v)) → (x : α) → α
hf : ∀ (x : (↑s : Type v)) (x_1 : α), f x x_1 ∈ (↑x : Set α) ∧ x_1 ≤ f x x_1
g : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) a (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) t
hg : BddAbove (Set.range g)
t : Set α
ht : t ∈ s
n : ℕ
w : (↑s : Type v)
⊢ Membership.mem (γ := Set α)
    (Set.range fun (x : (↑s : Type v)) ↦
      f x
        (Nat.rec (motive := fun (x : ℕ) ↦ α) a
          (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
    ((fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n)
have h : Eq.{v + 1} (α := α)
  ((fun (x : (↑s : Type v)) ↦
      f x
        (Nat.rec (motive := fun (x : ℕ) ↦ α) a
          (fun (x : ℕ) (IH : α) ↦ sSup (Set.range fun (x : (↑s : Type v)) ↦ f x IH)) n))
    (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht))
  ((fun (n : ℕ) ↦ f (Subtype.mk (p := fun (x : Set α) ↦ x ∈ s) t ht) (g n)) n)
Tactic: use ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂₀ Set.range f)
have refine : #(↑(Set.range f) : Type v) < cof α
Tactic: refine IsClub.sInter hα ?_ (by simpa)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ #(↑(Set.range f) : Type v) < cof α
have rw : lift.{u, v} #(↑(Set.range f) : Type v) < lift.{u, v} (cof α)
Tactic: rw [← Cardinal.lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
⊢ IsClub (s ∩ t)
have rw : IsClub (α := α) (⋂₀ {s, t})
Tactic: rw [← Set.sInter_pair]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (hypothesis)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
⊢ IsClub (α := α) (⋂₀ {s, t})
have H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
Tactic: have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
⊢ IsClub (α := α) (⋂₀ {s, t})
have inl : ∀ (hα : cof α < ℵ₀), IsClub (α := α) (⋂₀ {s, t})
Tactic: obtain hα | hα' := hα.lt_or_gt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
inl : ∀ (hα : cof α < ℵ₀), IsClub (α := α) (⋂₀ {s, t})
⊢ IsClub (α := α) (⋂₀ {s, t})
have inr : ∀ (hα' : ℵ₀ < cof α), IsClub (α := α) (⋂₀ {s, t})
Tactic: obtain hα | hα' := hα.lt_or_gt
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (hypothesis)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
s t : Set α
hα_1 : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
H : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → IsClub x
hα : cof α < ℵ₀
⊢ IsClub (α := α) (⋂₀ {s, t})
have hα₁ : cof α ≤ 1
Tactic: rw [cof_lt_aleph0_iff] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
⊢ IsClub (Function.fixedPoints f)
have inl : IsEmpty α → IsClub (Function.fixedPoints f)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
inl : IsEmpty α → IsClub (Function.fixedPoints f)
⊢ IsClub (Function.fixedPoints f)
have inr : Nonempty α → IsClub (Function.fixedPoints f)
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
⊢ IsClub (Function.fixedPoints f)
have inr : ∀ (s : Set α) (hs : s ⊆ Function.fixedPoints f) (hs₀ : s.Nonempty),
  DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → ∀ (a : α) (ha : IsLUB s a), IsLUB (f '' s) a
Tactic: refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
inr :
  ∀ (s : Set α) (hs : s ⊆ Function.fixedPoints f) (hs₀ : s.Nonempty),
    DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → ∀ (a : α) (ha : IsLUB s a), IsLUB (f '' s) a
⊢ IsClub (Function.fixedPoints f)
have inr₁ : ∀ (a : α), ∃ y ∈ Function.fixedPoints f, a ≤ y
Tactic: refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
h_1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ IsLUB (f '' s) a
have inr : IsLUB ((fun (a : α) ↦ a) '' s) a
Tactic: rwa [Set.image_congr hs, Set.image_id']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
a : α
val : OrderTop α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y
have h : ⊤ ∈ Function.fixedPoints f ∧ a ≤ ⊤
Tactic: use ⊤
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (hypothesis)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h : NoTopOrder α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y
have h₁ : NoMaxOrder α
Tactic: rw [noTopOrder_iff_noMaxOrder] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h : NoMaxOrder α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y
have inr : BddAbove.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)
Tactic: suffices BddAbove (.range fun n ↦ f^[n] a) from
        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h_1 : Nonempty α
a : α
h : NoMaxOrder α
⊢ BddAbove.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)
have inr : ∀ (h : IsCofinal.{v} (α := α) (Set.range fun (n : ℕ) ↦ f^[n] a)), #(↑(Set.range fun (n : ℕ) ↦ f^[n] a) : Type v) ≤ ℵ₀
Tactic: refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Club (goal)
Goal:
α : Type v
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h : Nonempty α
a : α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y
have inr : ∀ (x : OrderTop α ⊕' NoTopOrder α), ∃ y ∈ Function.fixedPoints f, a ≤ y
Tactic: cases topOrderOrNoTopOrder α with
    | inl => use ⊤; simpa using hf.strictMono.id_le ⊤
    | inr h =>
      rw [noTopOrder_iff_noMaxOrder] at h
      suffices BddAbove (.range fun n ↦ f^[n] a) from
        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
      refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
      simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
have inl : IsEmpty α → (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
inl : IsEmpty α → (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
have inr : Nonempty α → (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Cofinality.Enum (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : Subsingleton α
h : Nonempty α
⊢ (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
have inr : ∀ (val : Unique α), (type fun (x1 x2 : α) ↦ x1 < x2) ≤ (cof α).ord
Tactic: cases nonempty_unique α