mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ NoMaxOrder α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a ^ ω ∣ b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) a
b : Ordinal.{u_1}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a ^ b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ preOmega (ω + (a - ω)) = preOmega a

Tactic:
Ordinal.add_sub_cancel_of_le ha'

Goal state after:
case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ preOmega a = preOmega a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ range ⇑ω_ = {x | ω ≤ x ∧ x.IsInitial}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ ↔ ω ≤ x ∧ x.IsInitial

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preOmega o = ω_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preAleph o).ord = preOmega o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ typeLT Cardinal.{u} = Ordinal.univ.{u, u + 1}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ #Cardinal.{u} = univ.{u, u + 1}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ cof Cardinal.{u} = univ.{u, u + 1}

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ typeLT Cardinal.{u_1} ≤ (cof Cardinal.{u_1}).ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preAleph ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preAleph.symm ↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preAleph ω = ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preAleph.symm ℵ₀ = ω

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < preAleph o ↔ 0 < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ preAleph o ↔ ω ≤ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: ⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ preAleph c.ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (preOmega o) = preOmega (Ordinal.lift.{v, u} o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: ⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 2

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c * c = c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
ho : o ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ a ≤ a * b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ ℵ_ o₁ * ℵ_ o₂ = ℵ_ (max o₁ o₂)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ * ℵ_ o = ℵ_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ_ o * ℵ₀ = ℵ_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * succ b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
ho : o ≠ 0
⊢ ¬IsMin o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
⊢ preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : o ≠ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
⊢ a * b < c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ ¬IsMin o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a * b ≤ max a b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: f : Ordinal.{u_1} → Cardinal.{u_1}
hf : StrictMono f
o : Ordinal.{u_1}
⊢ preAleph o ≤ f o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: f : Ordinal.{u_1} → Cardinal.{u_1}
hf : StrictMono f
o : Ordinal.{u_1}
⊢ preAleph o ≤ f o

Tactic:
by
  simpa using (hf.comp preAleph.symm.strictMono).id_le (preAleph o)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
⊢ a * b = max a b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ b
⊢ a * b ≤ max a b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ succ (ℵ_ o) = ℵ_ (o + 1)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u}
ha : 0 < a
b : Ordinal.{u}
⊢ deriv (fun x ↦ a * x) b = a ^ ω * b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ_ (o + 1) = succ (ℵ_ o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ℵ_ 0 = ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} (ℵ_ o) = ℵ_ (Ordinal.lift.{v, u} o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
⊢ a * b = max a b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (ω_ o) = ω_ (Ordinal.lift.{v, u} o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ ℵ_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ < ℵ_ o ↔ 0 < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ cof ℤ = ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ Order.cof o.ToType = o.cof

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ Cardinal.lift.{v, u} o.cof = (lift.{v, u} o).cof

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ ℵ_ c.ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ Order.cof ↑(Iio o) = (lift.{u + 1, u} o).cof

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsSuccLimit (ω_ o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof ≤ o.card

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c.ord.cof ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 0 ↔ o = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < o.cof ↔ 0 < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ range ⇑ℵ_ = Ici ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 1 ↔ o ∈ range succ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ cof 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ∈ range ⇑ℵ_ ↔ ℵ₀ ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 < o.cof ↔ IsSuccLimit o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x o : Ordinal.{u_1}
⊢ x < ω_ o ↔ x.card < ℵ_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof < ℵ₀ ↔ o.cof ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ 1 < o.cof

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ IsSuccLimit o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ succ ℵ₀ = ℵ_ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ ℵ_ 1 ≤ c ↔ ℵ₀ < c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o.cof = ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < ℵ_ 1 ↔ c ≤ ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ℵ₀ < ℵ_ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
⊢ ℵ_ 1 ≤ #α ↔ Uncountable α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
inst✝ : Uncountable α
⊢ ℵ_ 1 ≤ #α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x1 x2 ↦ x1 * x2) ↑m ↑n < ω

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Countable ↔ #↑s < ℵ_ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preAleph o = ℵ_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ StrictMono preBeth

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
hb' : b ≠ 0
⊢ a * b = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
ha' : a ≠ 0
⊢ a * b = b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preBeth (o + 1) = 2 ^ preBeth o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ a * b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preBeth o = ⨆ a, preBeth ↑a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ ∃ s, IsCofinal s ∧ typeLT ↑s = (Order.cof α).ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ IsNormal preBeth

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth ↑0 = ↑((fun x ↦ 2 ^ x)^[0] 0)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preBeth ↑(n + 1) = ↑((fun x ↦ 2 ^ x)^[n + 1] 0)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: n : ℕ
⊢ preBeth ↑(n + 1) = ↑((fun x ↦ 2 ^ x)^[n + 1] 0)

Tactic:
by simp [Function.iterate_succ_apply', preBeth_nat]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
⊢ a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth ω = ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < preBeth o ↔ 0 < o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ preBeth c.ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preBeth o = 0 ↔ o = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
⊢ ∃ t ⊆ s, IsCofinal t ∧ typeLT ↑t = (Order.cof α).ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
⊢ ∃ t ⊆ s, IsCofinal t ∧ typeLT ↑t = (Order.cof α).ord

Tactic:
by
  obtain ⟨t, ht, ht'⟩ := exists_ord_cof_eq s
  rw [cof_eq_of_isCofinal hs] at ht'
  refine ⟨t, ?_, hs.trans ht, ?_⟩
  · simp
  · rw [← ht']
    exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinalType_congr.symm

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preBeth o).IsStrongPrelimit ↔ IsSuccPrelimit o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (preBeth o).IsStrongLimit ↔ IsSuccLimit o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (Order.cof α).ord.cof = Order.cof α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof.ord.cof = o.cof

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
⊢ b ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b = a ↔ max ℵ₀ b ≤ a ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
⊢ a + b = max a b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
⊢ #α + #α = #α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ ω + x✝¹ < ω + x✝

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ℶ_ 0 = ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℶ_ (o + 1) = 2 ^ ℶ_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ ℶ_ c.ord

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℶ_ o).IsStrongLimit ↔ IsSuccPrelimit o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ lift.{v, u_1} (ℶ_ o) = ℶ_ (Ordinal.lift.{v, u_1} o)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
· rcases le_or_gt ℵ₀ b with hb | hb
    · rw [add_comm, add_eq_max hb, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (add_lt_aleph0 ha hb).le

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preBeth o = ℶ_ o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ max a b
⊢ max a b + max a b < c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: γ : Type u
inst✝ : LinearOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = Order.cof γ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ_ 1 ≤ lift.{v, u} c ↔ ℵ_ 1 ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ_ 1 ↔ c ≤ ℵ_ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ_ 1 < lift.{v, u} c ↔ ℵ_ 1 < c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o ↔ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ_ 1 ↔ c < ℵ_ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
inst✝² : LinearOrder β
inst✝¹ : Small.{u, v} β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
⊢ Cardinal.lift.{v, u} (⨆ i, f i).cof = Cardinal.lift.{u, v} (Order.cof β)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: γ : Type u
inst✝¹ : LinearOrder γ
inst✝ : NoMaxOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i).cof = Order.cof γ

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
⊢ a * (ω * b) = ω * b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ_ 1 = lift.{v, u} c ↔ ℵ_ 1 = c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
h : a + b = c
ha : a < c
hc : ℵ₀ ≤ c
⊢ b = c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c = ℵ_ 1 ↔ c = ℵ_ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : b ≤ a
⊢ a + b = a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
⊢ b + a = b

Tactic:
add_eq_left hb ha

Goal state after:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
⊢ b = b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = a.cof

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n ≤ lift.{v, u} c ↔ ℵ_ ↑n ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
⊢ a + b = b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ ℵ_ ↑n ↔ c ≤ ℵ_ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n < lift.{v, u} c ↔ ℵ_ ↑n < c

Tactic:
by

Goal state after: