awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u}
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
hc : c.IsRegular
hs : #(↑s : Type u) < c
rw : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) ⋯) : Type u) < c ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
rw₁ : (∀ (i : (↑s : Type u)), #(↑(t (↑i : α) ⋯) : Type u) < c) ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
⊢ #(↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) : Type u) < c ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
have rw₂ : (∀ (i : (↑s : Type u)), #(↑(t (↑i : α) sorry) : Type u) < c) ↔ ∀ (x : (↑s : Type u)), #(↑(t (↑x : α) sorry) : Type u) < c
Tactic: rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ nfpFamily f a < c.ord
have apply : ℵ₀ < c.ord.cof
Tactic: apply nfpFamily_lt_ord_lift _ _ hf ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
apply : ℵ₀ < c.ord.cof
⊢ nfpFamily f a < c.ord
have apply₁ : lift.{v, u} #ι < c.ord.cof
Tactic: apply nfpFamily_lt_ord_lift _ _ hf ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c.ord.cof
have rw : ℵ₀ < c
Tactic: rw [hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c.ord.cof
have rw : ℵ₀ < c
Tactic: rw [hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c.ord.cof
have rw : ℵ₀ < c
Tactic: rw [hc.cof_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (hypothesis)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ a < c.ord → derivFamily f a < c.ord
have hω : ℵ₀ < c.ord.cof
Tactic: have hω : ℵ₀ < c.ord.cof := by
    rw [hc.cof_ord]
    exact lt_of_le_of_ne hc.1 hc'.symm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ 0 < c.ord → derivFamily f 0 < c.ord
have zero : 0 < c.ord → nfpFamily f 0 < c.ord
Tactic: rw [derivFamily_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ derivFamily f (b + 1) < c.ord
have add_one : nfpFamily f (derivFamily f b + 1) < c.ord
Tactic: rw [derivFamily_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ derivFamily f b < c.ord
have limit : ⨆ (b_1 : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑b_1 : Ordinal.{max u v}) < c.ord
Tactic: rw [derivFamily_limit f hb]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ ⨆ (b_1 : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑b_1 : Ordinal.{max u v}) < c.ord
have limit : lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) <
  (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof
Tactic: apply Ordinal.lift_iSup_lt_of_lt_cof
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
limit :
  lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) <
    (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof
⊢ ⨆ (b_1 : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑b_1 : Ordinal.{max u v}) < c.ord
have limit₁ : ∀ (i : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑i : Ordinal.{max u v}) < c.ord
Tactic: apply Ordinal.lift_iSup_lt_of_lt_cof
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) <
    (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof
have limit : lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c.ord.cof
Tactic: rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
limit :
  lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c.ord.cof
⊢ lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) <
    (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof
have limit₁ : lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c
Tactic: rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
limit :
  lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c.ord.cof
limit₁ : lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c
⊢ lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) <
    (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof
have limit₂ : lift.{max u v, max (u + 1) (v + 1)} (lift.{(max u v) + 1, max u v} b.card) < lift.{max (u + 1) (v + 1), max u v} c
Tactic: rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
limit :
  lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c.ord.cof
limit₁ : lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c
limit₂ :
  lift.{max u v, max (u + 1) (v + 1)} (lift.{(max u v) + 1, max u v} b.card) < lift.{max (u + 1) (v + 1), max u v} c
⊢ lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) <
    (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof
have limit₃ : lift.{max (max (u + 1) (v + 1)) u v, max u v} b.card < lift.{max (u + 1) (v + 1), max u v} c
Tactic: rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
limit :
  lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c.ord.cof
limit₁ : lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) < lift.{max (u + 1) (v + 1), max u v} c
limit₂ :
  lift.{max u v, max (u + 1) (v + 1)} (lift.{(max u v) + 1, max u v} b.card) < lift.{max (u + 1) (v + 1), max u v} c
limit₃ : lift.{max (max (u + 1) (v + 1)) u v, max u v} b.card < lift.{max (u + 1) (v + 1), max u v} c
⊢ lift.{max u v, max (u + 1) (v + 1)} #(↑(Iio b) : Type ((max u v) + 1)) <
    (Ordinal.lift.{max (u + 1) (v + 1), max u v} c.ord).cof
have limit₄ : b.card < c
Tactic: rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
hω : ℵ₀ < c.ord.cof
⊢ a < c.ord → derivFamily f a < c.ord
have zero : 0 < c.ord → derivFamily f 0 < c.ord
Tactic: induction a using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
  | add_one b hb =>
    intro hb'
    rw [derivFamily_add_one]
    exact
      nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
        ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
  | limit b hb H =>
    intro hb'
    rw [derivFamily_limit f hb]
    apply Ordinal.lift_iSup_lt_of_lt_cof
    · rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
    · exact fun i ↦ H i.1 i.2 <| i.2.trans hb'
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
hω : ℵ₀ < c.ord.cof
zero : 0 < c.ord → derivFamily f 0 < c.ord
⊢ a < c.ord → derivFamily f a < c.ord
have add_one : ∀ (b : Ordinal.{max u v}) (hb : b < c.ord → derivFamily f b < c.ord), b + 1 < c.ord → derivFamily f (b + 1) < c.ord
Tactic: induction a using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
  | add_one b hb =>
    intro hb'
    rw [derivFamily_add_one]
    exact
      nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
        ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
  | limit b hb H =>
    intro hb'
    rw [derivFamily_limit f hb]
    apply Ordinal.lift_iSup_lt_of_lt_cof
    · rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
    · exact fun i ↦ H i.1 i.2 <| i.2.trans hb'
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
hω : ℵ₀ < c.ord.cof
zero : 0 < c.ord → derivFamily f 0 < c.ord
add_one :
  ∀ (b : Ordinal.{max u v}) (hb : b < c.ord → derivFamily f b < c.ord), b + 1 < c.ord → derivFamily f (b + 1) < c.ord
⊢ a < c.ord → derivFamily f a < c.ord
have limit : ∀ (b : Ordinal.{max u v}) (hb : IsSuccLimit b) (H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord),
  b < c.ord → derivFamily f b < c.ord
Tactic: induction a using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
  | add_one b hb =>
    intro hb'
    rw [derivFamily_add_one]
    exact
      nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
        ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
  | limit b hb H =>
    intro hb'
    rw [derivFamily_limit f hb]
    apply Ordinal.lift_iSup_lt_of_lt_cof
    · rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]
    · exact fun i ↦ H i.1 i.2 <| i.2.trans hb'
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
⊢ ¬IsSingular.{u_1} (succ c)
have inl : ∀ (hc : c < ℵ₀), ¬IsSingular.{u_1} (succ c)
Tactic: obtain hc | hc := lt_or_ge c ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
inl : ∀ (hc : c < ℵ₀), ¬IsSingular.{u_1} (succ c)
⊢ ¬IsSingular.{u_1} (succ c)
have inr : ∀ (hc : ℵ₀ ≤ c), ¬IsSingular.{u_1} (succ c)
Tactic: obtain hc | hc := lt_or_ge c ℵ₀
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ¬IsSingular.{u_1} (succ c)
have inl : ∀ (n : ℕ) (hc : (↑n : Cardinal.{u_1}) < ℵ₀), ¬IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))
Tactic: obtain ⟨n, rfl⟩ := lt_aleph0.1 hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ ¬IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))
have inl : ∀ (h : IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))), succ (↑n : Cardinal.{u_1}) < ℵ₀
Tactic: refine fun h ↦ h.aleph0_le.not_gt ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
h : IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))
⊢ succ (↑n : Cardinal.{u_1}) < ℵ₀
have inl : (↑(n + 1) : Cardinal.{u_1}) < ℵ₀
Tactic: rw [succ_natCast, ← Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ IsSuccLimit c
have rw : c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c
Tactic: rw [Cardinal.isSuccLimit_iff, isSuccPrelimit_iff_succ_ne]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c
have refine : ∀ (b : Cardinal.{u_1}), succ b ≠ c
Tactic: refine ⟨hc.pos.ne', ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ c.IsSingular
have rw : c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof
Tactic: rw [isSingular_iff, ← (cof_ord_le c).lt_iff_ne, ← not_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof
have left : ¬c.IsRegular → ℵ₀ ≤ c
Tactic: tauto
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
left : ¬c.IsRegular → ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof
have right : ¬c.IsRegular → ¬c ≤ c.ord.cof
Tactic: tauto
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (hypothesis)
Goal:
c : Cardinal.{u_1}
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular
have this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
Tactic: have := isRegular_or_isSingular (c := c)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular
have rw : ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
Tactic: rw [← not_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr₄ : ∀ (this : c.IsRegular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₄ : ∀ (this : c.IsRegular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr₅ : ∀ (this : c.IsSingular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₄ : ∀ (this : c.IsRegular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₅ : ∀ (this : c.IsSingular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inl₃ : ∀ (this : ¬ℵ₀ ≤ c), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₄ : ∀ (this : c.IsRegular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₅ : ∀ (this : c.IsSingular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inl₃ : ∀ (this : ¬ℵ₀ ≤ c), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr₆ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₄ : ∀ (this : c.IsRegular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₅ : ∀ (this : c.IsSingular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inl₃ : ∀ (this : ¬ℵ₀ ≤ c), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₆ inr₇ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr₈ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → ¬c.IsRegular → c.IsSingular
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Regular (goal)
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
inl : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₁ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₁ : ∀ (this : ¬ℵ₀ ≤ c), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₂ : ∀ (this : c.IsRegular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inr₃ : ∀ (this : c.IsSingular), ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
inl₂ : ∀ (this : ¬ℵ₀ ≤ c), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₄ : ∀ (this : c.IsRegular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₅ : ∀ (this : c.IsSingular), ¬¬ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inl₃ : ∀ (this : ¬ℵ₀ ≤ c), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₆ inr₇ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₈ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → ¬c.IsRegular → c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
have inr₉ : ∀ (this : c.IsSingular), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
Tactic: tauto
Cleared hypotheses: this