awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
h : IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))
inl : (↑(n + 1) : Cardinal.{u_1}) < ℵ₀
⊢ succ (↑n : Cardinal.{u_1}) < ℵ₀

Tactic:
rw [succ_natCast, ← Nat.cast_add_one]

Premises used: Cardinal.succ_natCast, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
h : IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))
⊢ (↑(n + 1) : Cardinal.{u_1}) < ℵ₀

Tactic:
natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
n : ℕ
hc : (↑n : Cardinal.{u_1}) < ℵ₀
h : IsSingular.{u_1} (succ (↑n : Cardinal.{u_1}))
⊢ (↑(n + 1) : Cardinal.{u_1}) < ℵ₀

Tactic:
exact natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬IsSingular.{u_1} (succ c)

Tactic:
(isRegular_succ hc).not_isSingular

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

Tactic:
exact (isRegular_succ hc).not_isSingular

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

Tactic:
simp [← succ_aleph]

Premises used: Cardinal.succ_aleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
rw : c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c
⊢ IsSuccLimit c

Tactic:
rw [Cardinal.isSuccLimit_iff, isSuccPrelimit_iff_succ_ne]

Premises used: Cardinal.isSuccLimit_iff, Order.isSuccPrelimit_iff_succ_ne
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c

Tactic:
⟨hc.pos.ne', ?_⟩

Premises used: Cardinal.IsSingular.pos, LT.lt.ne', And.intro
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
refine : ∀ (b : Cardinal.{u_1}), succ b ≠ c
⊢ c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c

Tactic:
refine ⟨hc.pos.ne', ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : IsSingular.{u_1} (succ c)
⊢ False

Tactic:
not_isSingular_succ c hc

Premises used: Cardinal.not_isSingular_succ
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : IsSingular.{u_1} (succ c)
⊢ False

Tactic:
exact not_isSingular_succ c hc

Premises used: Cardinal.not_isSingular_succ
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rw : c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof
⊢ c.IsRegular ∨ c.IsSingular

Tactic:
rw [isSingular_iff, ← (cof_ord_le c).lt_iff_ne, ← not_le]

Premises used: not_le, Cardinal.isSingular_iff, LE.le.lt_iff_ne, Ordinal.cof_ord_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
left : ¬c.IsRegular → ℵ₀ ≤ c
right : ¬c.IsRegular → ¬c ≤ c.ord.cof
right₁ right₂ right₃ right₄ right₅ right₆ right₇ right₈ : ¬c.IsRegular → c ≤ c.ord.cof → False
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof

Tactic:
tauto
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
⊢ ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular

Tactic:
have := isRegular_or_isSingular (c := c)
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
this : ∀ (h : ℵ₀ ≤ c), c.IsRegular ∨ c.IsSingular
rw : ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular

Tactic:
rw [← not_le]

Premises used: not_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
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
inr₉ inr₁₀ : ∀ (this : c.IsSingular), ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
inr₁₁ : ∀ (this : c.IsSingular), ℵ₀ ≤ c → ¬c.IsRegular → c.IsSingular
inr₁₂ : ∀ (this : c.IsRegular), ℵ₀ ≤ c → ¬c.IsRegular → c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular

Tactic:
tauto
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h₀ : ℵ₀ ≤ c
hc : ¬c.IsRegular
⊢ c.IsSingular

Tactic:
(isRegular_or_isSingular h₀).resolve_left hc

Premises used: Or.resolve_left, Cardinal.isRegular_or_isSingular
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h₀ : ℵ₀ ≤ c
hc : ¬c.IsSingular
⊢ c.IsRegular

Tactic:
(isRegular_or_isSingular h₀).resolve_right hc

Premises used: Cardinal.isRegular_or_isSingular, Or.resolve_right
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
inl :
  IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0) ↔
    IsSuccLimit.{u_1 + 1} (α := Ordinal.{u_1}) 0 ∧ Ordinal.cof 0 < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0
inr :
  ∀ (a : Ordinal.{u_1}),
    IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)) ↔
      IsSuccLimit (succ a) ∧ (succ a).cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)
inr₁ :
  ∀ (ho : IsSuccLimit o),
    IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
      IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
obtain rfl | ⟨a, rfl⟩ | ho := zero_or_succ_or_isSuccLimit o

Premises used: Ordinal.zero_or_succ_or_isSuccLimit, rfl
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0) ↔
    IsSuccLimit.{u_1 + 1} (α := Ordinal.{u_1}) 0 ∧ Ordinal.cof 0 < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
a : Ordinal.{u_1}
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)) ↔
    IsSuccLimit (succ a) ∧ (succ a).cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ a)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
inr :
  ℵ₀ ≤ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ∧
      (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)).cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
rw [isSingular_iff, ← (cof_ord_le _).lt_iff_ne]

Premises used: Cardinal.isSingular_iff, LE.le.lt_iff_ne, Ordinal.cof_ord_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ ℵ₀ ≤ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ∧
      (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)).cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔
    IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
simp [ho]
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
hc : IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)
⊢ IsSuccLimit o

Tactic:
(isSingular_aleph_iff.1 hc).1

Premises used: Cardinal.isSingular_aleph_iff, And.left, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω)

Tactic:
simp [isSingular_aleph_iff]

Premises used: Cardinal.isSingular_aleph_iff
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsSingular
obtain :
  ∀ (o : Ordinal.{u_1}) (hc : IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)),
    LE.le (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω : Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω ≤ c

Tactic:
obtain ⟨o, rfl⟩ := mem_range_aleph_iff.2 hc.aleph0_le

Premises used: Iff.mpr, Cardinal.IsSingular.aleph0_le, Cardinal.mem_range_aleph_iff, rfl
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
hc : IsSingular.{u_1} ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o)
⊢ IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
rw [isSingular_aleph_iff] at hc

Premises used: Cardinal.isSingular_aleph_iff
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
rw : ω ≤ o
⊢ LE.le (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})

Tactic:
rw [aleph_le_aleph]

Premises used: Cardinal.aleph_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ ω ≤ o

Tactic:
omega0_le_of_isSuccLimit hc.1

Premises used: And.left, Ordinal.omega0_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ ω ≤ o

Tactic:
exact omega0_le_of_isSuccLimit hc.1

Premises used: And.left, Ordinal.omega0_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : c.IsInaccessible
n : ℕ
⊢ (↑n : Cardinal.{u_1}) < c

Tactic:
natCast_lt_aleph0.trans h.1

Premises used: Cardinal.IsInaccessible.aleph0_lt, Cardinal.natCast_lt_aleph0, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : c.IsInaccessible
⊢ 0 < c

Tactic:
aleph0_pos.trans h.1

Premises used: Cardinal.IsInaccessible.aleph0_lt, LT.lt.trans, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : c.IsInaccessible
⊢ c ≠ 0

Tactic:
h.pos.ne'

Premises used: Cardinal.IsInaccessible.pos, LT.lt.ne'
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : c.IsInaccessible
⊢ c.IsRegular

Tactic:
⟨h.aleph0_lt.le, h.le_cof_ord⟩

Premises used: Cardinal.IsRegular.mk, Cardinal.IsInaccessible.aleph0_lt, LT.lt.le, Cardinal.IsInaccessible.le_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : c.IsInaccessible
⊢ c.IsStrongLimit

Tactic:
⟨h.ne_zero, h.isStrongPrelimit⟩

Premises used: Cardinal.IsStrongLimit.mk, Cardinal.IsInaccessible.isStrongPrelimit, Cardinal.IsInaccessible.ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
h : c.IsInaccessible
⊢ IsSuccLimit c

Tactic:
h.isStrongLimit.isSuccLimit

Premises used: Cardinal.IsStrongLimit.isSuccLimit, Cardinal.IsInaccessible.isStrongLimit
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ Cardinal.univ.{u, v} ≤ Cardinal.univ.{u, v}.ord.cof

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
apply : (preBeth ∘ ord) c ≤ c
⊢ preBeth c.ord = c

Tactic:
apply (preBeth_strictMono.comp ord_strictMono).le_apply.antisymm'

Premises used: StrictMono.le_apply, LE.le.antisymm', Cardinal.ord_strictMono, Cardinal.preBeth_strictMono, StrictMono.comp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
apply : ∀ a' < c.ord, preBeth a' ≤ c
⊢ (preBeth ∘ ord) c ≤ c

Tactic:
apply (isNormal_preBeth.le_iff_forall_le (isSuccLimit_ord hc.aleph0_lt.le)).2

Premises used: Iff.mpr, Cardinal.isSuccLimit_ord, Cardinal.IsInaccessible.aleph0_lt, LT.lt.le, Order.IsNormal.le_iff_forall_le, Cardinal.isNormal_preBeth
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ∀ a' < c.ord, preBeth a' ≤ c

Tactic:
fun a ha ↦ le_of_lt ?_

Premises used: le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
refine : ∀ (a : Ordinal.{u_1}) (ha : a < c.ord), preBeth a < c
⊢ ∀ a' < c.ord, preBeth a' ≤ c

Tactic:
refine fun a ha ↦ le_of_lt ?_

Premises used: le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
ha : a < c.ord
ind : ∀ (a : Ordinal.{u_1}) (IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c) (ha : a < c.ord), preBeth a < c
⊢ preBeth a < c

Tactic:
induction a using WellFoundedLT.induction with | ind a IH

Premises used: WellFoundedLT.induction
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
ind : ⨆ (a_1 : (↑(Iio a) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a_1 : Ordinal.{u_1})) < c
⊢ preBeth a < c

Tactic:
rw [preBeth]

Premises used: Cardinal.preBeth
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
apply : lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof
apply₁ : ∀ (i : (↑(Iio a) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑i : Ordinal.{u_1})) < c
⊢ ⨆ (a_1 : (↑(Iio a) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a_1 : Ordinal.{u_1})) < c

Tactic:
apply lift_iSup_lt_of_lt_cof_ord _ _

Premises used: Cardinal.lift_iSup_lt_of_lt_cof_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
rwa : lift.{u_1, u_1 + 1} (lift.{u_1 + 1, u_1} a.card) < (lift.{u_1 + 1, u_1} c).ord.cof
rwa₁ : lift.{u_1 + 1, u_1} a.card < (lift.{u_1 + 1, u_1} c).ord.cof
rwa₂ : lift.{u_1 + 1, u_1} a.card < lift.{u_1 + 1, u_1} c
rwa₃ : a.card < c
rwa₄ rwa₅ rwa₆ rwa₇ : a < c.ord
⊢ lift.{u_1, u_1 + 1} #(↑(Iio a) : Type (u_1 + 1)) < (lift.{u_1 + 1, u_1} c).ord.cof

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

Premises used: Cardinal.lift_lift, Cardinal.IsRegular.cof_ord, Cardinal.IsInaccessible.isRegular, Cardinal.mk_Iio_ordinal, Cardinal.lift_lt, Cardinal.IsRegular.lift, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
b : Ordinal.{u_1}
hb : b ∈ Iio a
⊢ HPow.hPow (α := Cardinal.{u_1}) 2
      (preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio a) b hb) : Ordinal.{u_1})) <
    c

Tactic:
hc.isStrongPrelimit <| IH _ hb (hb.trans ha)

Premises used: Cardinal.IsInaccessible.isStrongPrelimit, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, ∀ (ha : y < c.ord), preBeth y < c
ha : a < c.ord
b : Ordinal.{u_1}
hb : b ∈ Iio a
⊢ HPow.hPow (α := Cardinal.{u_1}) 2
      (preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio a) b hb) : Ordinal.{u_1})) <
    c

Tactic:
exact hc.isStrongPrelimit <| IH _ hb (hb.trans ha)

Premises used: Cardinal.IsInaccessible.isStrongPrelimit, LT.lt.trans
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
rw : HPow.hPow (β := ℕ) ω 2 < c.ord
⊢ ℶ_ c.ord = c

Tactic:
rw [← preBeth_of_omega0_sq_le (le_of_lt _), hc.preBeth_ord]

Premises used: Cardinal.IsInaccessible.preBeth_ord, le_of_lt, Cardinal.preBeth_of_omega0_sq_le
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
rw : ℵ₀ < c
⊢ HPow.hPow (β := ℕ) ω 2 < c.ord

Tactic:
rw [lt_ord, pow_two, card_mul, card_omega0, aleph0_mul_aleph0]

Premises used: pow_two, Ordinal.card_omega0, Ordinal.card_mul, Cardinal.lt_ord, Cardinal.aleph0_mul_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ < c

Tactic:
hc.aleph0_lt

Premises used: Cardinal.IsInaccessible.aleph0_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ < c

Tactic:
exact hc.aleph0_lt

Premises used: Cardinal.IsInaccessible.aleph0_lt
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord = c

Tactic:
((preAleph_le_preBeth _).trans hc.preBeth_ord.le).antisymm
    (preAleph.strictMono.comp ord_strictMono).le_apply

Premises used: StrictMono.le_apply, OrderIso.strictMono, Cardinal.IsInaccessible.preBeth_ord, LE.le.antisymm, Eq.le, Cardinal.preAleph, Cardinal.ord_strictMono, Cardinal.preAleph_le_preBeth, LE.le.trans, StrictMono.comp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord = c

Tactic:
((aleph_le_beth _).trans hc.beth_ord.le).antisymm (aleph.strictMono.comp ord_strictMono).le_apply

Premises used: Cardinal.aleph_le_beth, StrictMono.le_apply, Cardinal.aleph, OrderEmbedding.strictMono, LE.le.antisymm, Eq.le, Cardinal.IsInaccessible.beth_ord, Cardinal.ord_strictMono, LE.le.trans, StrictMono.comp
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
rw : ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord) = c.ord
rw₁ rw₂ : c.ord = c.ord
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) c.ord = c.ord

Tactic:
rw [← ord_preAleph, hc.preAleph_ord]

Premises used: Cardinal.IsInaccessible.preAleph_ord, Cardinal.ord_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
c : Cardinal.{u_1}
hc : c.IsInaccessible
rw : ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord) = c.ord
rw₁ rw₂ : c.ord = c.ord
⊢ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) c.ord = c.ord

Tactic:
rw [← ord_aleph, hc.aleph_ord]

Premises used: Cardinal.ord_aleph, Cardinal.IsInaccessible.aleph_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ preBeth Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.preBeth_ord

Premises used: Cardinal.IsInaccessible.preBeth_ord, Cardinal.IsInaccessible.univ
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ ℶ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.beth_ord

Premises used: Cardinal.IsInaccessible.univ, Cardinal.IsInaccessible.beth_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ (preAleph : (a : Ordinal.{max (u + 1) v}) → Cardinal.{max (u + 1) v}) Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.preAleph_ord

Premises used: Cardinal.IsInaccessible.preAleph_ord, Cardinal.IsInaccessible.univ
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ (ℵ_ : (a : Ordinal.{max (u + 1) v}) → Cardinal.{max (u + 1) v}) Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.aleph_ord

Premises used: Cardinal.IsInaccessible.univ, Cardinal.IsInaccessible.aleph_ord
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ (preOmega : (a : Ordinal.{max (u + 1) v}) → Ordinal.{max (u + 1) v}) Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.preOmega_ord

Premises used: Cardinal.IsInaccessible.preOmega_ord, Cardinal.IsInaccessible.univ
-- Module: Mathlib.SetTheory.Cardinal.Regular
Goal:
⊢ (ω_ : (a : Ordinal.{max (u + 1) v}) → Ordinal.{max (u + 1) v}) Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
simpa using IsInaccessible.univ.omega_ord

Premises used: Cardinal.IsInaccessible.omega_ord, Cardinal.IsInaccessible.univ
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
inl : ∀ (hβ : IsEmpty β), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
inr : ∀ (hβ : Nonempty β), ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
rcases isEmpty_or_nonempty β with hβ | hβ

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : IsEmpty β
⊢ IsEmpty α

Tactic:
have : IsEmpty α := Function.isEmpty f
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : IsEmpty β
this : IsEmpty α
⊢ ∀ (a : α), R a (((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm : (a : α) → β) a)

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : IsEmpty β
this : IsEmpty α
⊢ ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective, by simp⟩
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
s t : Set α
hst : s ⊆ t
⊢ (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F
⊢ (g '' (f '' s)ᶜ)ᶜ = s

Tactic:
have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ (g '' (f '' s)ᶜ)ᶜ = sᶜᶜ

Tactic:
simp [hs]
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ g '' (f '' s)ᶜ = sᶜ

Tactic:
have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
⊢ LeftInverse g' g

Tactic:
have g'g : LeftInverse g' g := leftInverse_invFun hg
-- Module: Mathlib.SetTheory.Cardinal.SchroederBernstein
Goal:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun (s : Set α) ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := (OrderHom.lfp : (a : Set α →o Set α) → Set α) F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
rw : g' '' g '' (f '' s)ᶜ = (f '' s)ᶜ
rw₁ rw₂ : (f '' s)ᶜ = (f '' s)ᶜ
⊢ g' '' sᶜ = (f '' s)ᶜ

Tactic:
rw [← hns, g'g.image_image]

Premises used: Function.LeftInverse.image_image