awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι rwa rwa₁ rwa₂ rwa₃ : lift.{v, u} o.card < c
⊢ lift.{v, u} o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι rwa rwa₁ rwa₂ rwa₃ : o.card < c
⊢ o.card < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
apply : lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
⊢ iSup f < c

Tactic:
apply lift_iSup_lt_of_lt_cof_ord _ hf

Premises used: Cardinal.lift_iSup_lt_of_lt_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
rwa : lift.{v, u} #ι < (lift.{u, max u v} c).ord.cof
rwa₁ : lift.{v, u} #ι < c.ord.cof
rwa₂ rwa₃ rwa₄ rwa₅ : lift.{v, u} #ι < c
⊢ lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof

Tactic:
rwa [lift_umax, c.lift_id', hc.cof_ord]

Premises used: Cardinal.lift_id', Cardinal.IsRegular.cof_ord, Cardinal.lift_umax
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι : Type u_1
f : ι → Cardinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι rwa rwa₁ rwa₂ rwa₃ : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
apply : lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof
⊢ sum f < c

Tactic:
apply (sum_le_lift_mk_mul_iSup _).trans_lt <|
    mul_lt_of_lt hc.1 hι (lift_iSup_lt_of_lt_cof_ord _ hf)

Premises used: Cardinal.IsRegular.aleph0_le, Cardinal.sum_le_lift_mk_mul_iSup, Cardinal.mul_lt_of_lt, Cardinal.lift_iSup_lt_of_lt_cof_ord, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
rwa : lift.{v, u} #ι < (lift.{u, max u v} c).ord.cof
rwa₁ : lift.{v, u} #ι < c.ord.cof
rwa₂ rwa₃ rwa₄ rwa₅ : lift.{v, u} #ι < c
⊢ lift.{max u v, u} #ι < (lift.{u, max u v} c).ord.cof

Tactic:
rwa [lift_umax, c.lift_id', hc.cof_ord]

Premises used: Cardinal.lift_id', Cardinal.IsRegular.cof_ord, Cardinal.lift_umax
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι : Type u
f : ι → Cardinal.{u}
hc : c.IsRegular
hι rwa rwa₁ rwa₂ rwa₃ : #ι < c
⊢ lift.{u, u} #ι < c

Tactic:
rwa [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι α : Type u
t : ι → Set α
c : Cardinal.{u}
h : #(↑(⋃ (i : ι), t i) : Type u) < c
i : ι
⊢ #(↑(t i) : Type u) < c

Tactic:
lt_of_le_of_lt (Cardinal.mk_le_mk_of_subset <| subset_iUnion _ _) h

Premises used: lt_of_le_of_lt, Set.subset_iUnion, Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
⊢ #(↑(⋃ (i : ι), t i) : Type u) < c ↔ ∀ (i : ι), #(↑(t i) : Type u) < c

Tactic:
⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩

Premises used: Cardinal.card_lt_of_card_iUnion_lt, Iff.intro
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
refine : ∀ (h : ∀ (i : ι), #(↑(t i) : Type u) < c), #(↑(⋃ (i : ι), t i) : Type u) < c
⊢ #(↑(⋃ (i : ι), t i) : Type u) < c ↔ ∀ (i : ι), #(↑(t i) : Type u) < c

Tactic:
refine ⟨card_lt_of_card_iUnion_lt, fun h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
apply :
  #(↑(range fun (i : ι) ↦ t i) : Type u) * ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c
⊢ #(↑(⋃ (i : ι), t i) : Type u) < c

Tactic:
apply lt_of_le_of_lt (Cardinal.mk_sUnion_le _)

Premises used: Cardinal.mk_sUnion_le, lt_of_le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
apply : ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c
⊢ #(↑(range fun (i : ι) ↦ t i) : Type u) * ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c

Tactic:
apply Cardinal.mul_lt_of_lt hc.aleph0_le (mk_range_le.trans_lt hι)

Premises used: Cardinal.IsRegular.aleph0_le, Cardinal.mk_range_le, Cardinal.mul_lt_of_lt, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
apply : ∀ (i : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑i : Set α) : Type u) < c
apply₁ : #ι < c.ord.cof
⊢ ⨆ (s : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑s : Set α) : Type u) < c

Tactic:
apply Cardinal.iSup_lt_of_lt_cof_ord (mk_range_le.trans_lt _)

Premises used: Cardinal.iSup_lt_of_lt_cof_ord, Cardinal.mk_range_le, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
⊢ ∀ (i : (↑(range fun (i : ι) ↦ t i) : Type u)), #(↑(↑i : Set α) : Type u) < c

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u}
ι α : Type u
t : ι → Set α
hc : c.IsRegular
hι : #ι < c
h : ∀ (i : ι), #(↑(t i) : Type u) < c
rwa rwa₁ rwa₂ rwa₃ : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #(↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) : Type u) < c
a : α
ha : a ∈ s
rw : ∀ (h : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) ⋯) : Type u) < c) (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c
⊢ #(↑(t a ha) : Type u) < c

Tactic:
rw [biUnion_eq_iUnion] at h

Premises used: Set.biUnion_eq_iUnion
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) ⋯) : Type u) < c
a : α
ha : a ∈ s
⊢ ∀ (i : (↑s : Type u)), #(↑(t (↑i : α) ⋯) : Type u) < c

Tactic:
have := card_lt_of_card_iUnion_lt h
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #(↑(⋃ (x : (↑s : Type u)), t (↑x : α) ⋯) : Type u) < c
a : α
ha : a ∈ s
this : ∀ (i : (↑s : Type u)), #(↑(t (↑i : α) ⋯) : Type u) < c
⊢ #(↑(t a ha) : Type u) < c

Tactic:
simp_all only [iUnion_coe_set, Subtype.forall]

Premises used: Set.iUnion_coe_set, Subtype.forall
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rw₂ rw₃ :
  (∀ (i : (↑s : Type u)), #(↑(t (↑i : α) ⋯) : Type u) < c) ↔ ∀ (x : (↑s : Type u)), #(↑(t (↑x : α) ⋯) : Type u) < c
⊢ #(↑(⋃ (a : α), ⋃ (h : a ∈ s), t a h) : Type u) < c ↔ ∀ (a : α) (ha : a ∈ s), #(↑(t a ha) : Type u) < c

Tactic:
rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']

Premises used: Cardinal.card_iUnion_lt_iff_forall_of_isRegular, Set.biUnion_eq_iUnion, SetCoe.forall'
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
apply₁ : lift.{v, u} #ι < c.ord.cof
⊢ nfpFamily f a < c.ord

Tactic:
apply nfpFamily_lt_ord_lift _ _ hf ha

Premises used: Ordinal.nfpFamily_lt_ord_lift
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rw : ℵ₀ < c
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rw : lift.{v, u} #ι < c
⊢ lift.{v, u} #ι < c.ord.cof

Tactic:
rw [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
lt_of_le_of_ne hc.1 hc'.symm

Premises used: Cardinal.IsRegular.aleph0_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
exact lt_of_le_of_ne hc.1 hc'.symm

Premises used: Cardinal.IsRegular.aleph0_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
⊢ lift.{v, u} #ι < c

Tactic:
hι
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
⊢ lift.{v, u} #ι < c

Tactic:
exact hι
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
a : Ordinal.{u}
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
rwa rwa₁ rwa₂ rwa₃ : #ι < c
⊢ lift.{u, u} #ι < c

Tactic:
rwa [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Regular
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}
rw : ℵ₀ < c
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
lt_of_le_of_ne hc.1 hc'.symm

Premises used: Cardinal.IsRegular.aleph0_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
exact lt_of_le_of_ne hc.1 hc'.symm

Premises used: Cardinal.IsRegular.aleph0_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
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}
rw : ℵ₀ < c
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
lt_of_le_of_ne hc.1 hc'.symm

Premises used: Cardinal.IsRegular.aleph0_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
exact lt_of_le_of_ne hc.1 hc'.symm

Premises used: Cardinal.IsRegular.aleph0_le, Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
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

Tactic:
have hω : ℵ₀ < c.ord.cof := by
    rw [hc.cof_ord]
    exact lt_of_le_of_ne hc.1 hc'.symm
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
zero : 0 < c.ord → nfpFamily f 0 < c.ord
⊢ 0 < c.ord → derivFamily f 0 < c.ord

Tactic:
rw [derivFamily_zero]

Premises used: Ordinal.derivFamily_zero
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rwa rwa₁ rwa₂ rwa₃ : lift.{v, u} #ι < c
⊢ lift.{v, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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 → nfpFamily f 0 < c.ord

Tactic:
exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf

Premises used: Ordinal.nfpFamily_lt_ord_lift
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
add_one : nfpFamily f (derivFamily f b + 1) < c.ord
⊢ derivFamily f (b + 1) < c.ord

Tactic:
rw [derivFamily_add_one]

Premises used: Ordinal.derivFamily_add_one
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
rwa rwa₁ rwa₂ rwa₃ : lift.{v, u} #ι < c
⊢ lift.{v, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_ord]

Premises used: Cardinal.IsRegular.cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
⊢ nfpFamily f (derivFamily f b + 1) < c.ord

Tactic:
exact
      nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
        ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))

Premises used: Cardinal.isSuccLimit_ord, Cardinal.IsRegular.aleph0_le, Ordinal.nfpFamily_lt_ord_lift, Order.lt_succ, Order.IsSuccLimit.succ_lt, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.Regular
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 : ⨆ (b_1 : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑b_1 : Ordinal.{max u v}) < c.ord
⊢ derivFamily f b < c.ord

Tactic:
rw [derivFamily_limit f hb]

Premises used: Ordinal.derivFamily_limit
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
limit₁ : ∀ (i : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑i : Ordinal.{max u v}) < c.ord
⊢ ⨆ (b_1 : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑b_1 : Ordinal.{max u v}) < c.ord

Tactic:
apply Ordinal.lift_iSup_lt_of_lt_cof

Premises used: Ordinal.lift_iSup_lt_of_lt_cof
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
limit₄ : b.card < c
limit₅ limit₆ limit₇ limit₈ : 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

Tactic:
rwa [← lift_cof, hc.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord]

Premises used: Cardinal.lift_lift, Cardinal.IsRegular.cof_ord, Cardinal.mk_Iio_ordinal, Cardinal.lift_lt, Ordinal.lift_cof, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
⊢ ∀ (i : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑i : Ordinal.{max u v}) < c.ord

Tactic:
fun i ↦ H i.1 i.2 <| i.2.trans hb'

Premises used: LT.lt.trans, Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
⊢ ∀ (i : (↑(Iio b) : Type ((max u v) + 1))), derivFamily f (↑i : Ordinal.{max u v}) < c.ord

Tactic:
exact fun i ↦ H i.1 i.2 <| i.2.trans hb'
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
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
⊢ a < c.ord → derivFamily f a < 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'

Premises used: Cardinal.lift_lift, Ordinal.nfpFamily_lt_ord_lift, Ordinal.derivFamily_add_one, Cardinal.IsRegular.cof_ord, Cardinal.mk_Iio_ordinal, Cardinal.lift_lt, Ordinal.lift_cof, Ordinal.zero, Ordinal.derivFamily_zero, Ordinal.lift_iSup_lt_of_lt_cof, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{u}
rwa rwa₁ rwa₂ rwa₃ : #ι < c
⊢ lift.{u, u} #ι < c

Tactic:
rwa [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
f : Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u}
⊢ lift.{u, 0} #Unit < c

Tactic:
simpa using Cardinal.one_lt_aleph0.trans (lt_of_le_of_ne hc.1 hc'.symm)

Premises used: Cardinal.one_lt_aleph0, Cardinal.IsRegular.aleph0_le, Ne.symm, LT.lt.trans, lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ c.ord.cof < c

Tactic:
(cof_ord_le c).lt_of_ne hc.cof_ord_ne

Premises used: Cardinal.IsSingular.cof_ord_ne, LE.le.lt_of_ne, Ordinal.cof_ord_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
n : ℕ
⊢ (↑n : Cardinal.{u_1}) < c

Tactic:
natCast_lt_aleph0.trans_le hc.aleph0_le

Premises used: Cardinal.natCast_lt_aleph0, LT.lt.trans_le, Cardinal.IsSingular.aleph0_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ 0 < c

Tactic:
hc.natCast_lt 0

Premises used: Cardinal.IsSingular.natCast_lt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ ¬c.IsRegular

Tactic:
fun hc' ↦ hc'.le_cof_ord.not_gt hc.cof_ord_lt

Premises used: Cardinal.IsSingular.cof_ord_lt, LE.le.not_gt, Not, Cardinal.IsRegular.le_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsRegular
⊢ ¬c.IsSingular

Tactic:
imp_not_comm.1 IsSingular.not_isRegular hc

Premises used: Cardinal.IsSingular.not_isRegular, imp_not_comm, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ ¬ℵ₀.IsSingular

Tactic:
isRegular_aleph0.not_isSingular

Premises used: Cardinal.isRegular_aleph0, Cardinal.IsRegular.not_isSingular
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ ¬IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)

Tactic:
isRegular_aleph_one.not_isSingular

Premises used: Cardinal.isRegular_aleph_one, Cardinal.IsRegular.not_isSingular
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
inl : ∀ (hc : c < ℵ₀), ¬IsSingular.{u_1} (succ c)
inr : ∀ (hc : ℵ₀ ≤ c), ¬IsSingular.{u_1} (succ c)
⊢ ¬IsSingular.{u_1} (succ c)

Tactic:
obtain hc | hc := lt_or_ge c ℵ₀

Premises used: Cardinal.aleph0, lt_or_ge
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c < ℵ₀
inl : ∀ (n : ℕ) (hc : (↑n : Cardinal.{u_1}) < ℵ₀), ¬IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))
⊢ ¬IsSingular.{u_1} (succ c)

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 hc

Premises used: Iff.mp, Cardinal.lt_aleph0, rfl
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
⊢ ¬IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))

Tactic:
fun h ↦ h.aleph0_le.not_gt ?_

Premises used: LE.le.not_gt, Cardinal.IsSingular.aleph0_le, Not
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
inl : ∀ (h : IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))), succ (↑n : Cardinal.{u_1}) < ℵ₀
⊢ ¬IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))

Tactic:
refine fun h ↦ h.aleph0_le.not_gt ?_