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

Goal state before:
pp: case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ (c * b))

Tactic:
]

Goal state after:
case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ (c * b))
Module: Mathlib.SetTheory.Ordinal.Principal

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

Tactic:
]

Goal state after:
case inl
b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
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:
]

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

Goal state before:
pp: case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0

Tactic:
]

Goal state after:
case inr.inl
a : Ordinal.{u}
h✝ : 0 < a
hb₁ : 0 ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
]

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω

Tactic:
]

Goal state after:
case a.ab
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * b + c ≤ a ^ ω * b + a ^ ω
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = ω_ o
Module: Mathlib.SetTheory.Cardinal.Aleph

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

pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ ω < ω ^ ↑2

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ ω < ω ^ ↑2
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ ((typein s).toRelEmbedding p).card < #α

Tactic:
]

Goal state after:
case ind.mk
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
⊢ ((typein s).toRelEmbedding p).card < #α
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c' < b, c < a * c'
hd : ∃ c' < b, d < a * c'
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'

Tactic:
]

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c' < b, c < a * c'
hd : ∃ c' < b, d < a * c'
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a ^ ω * succ b ≤ a ^ ω * succ b

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
⊢ a ^ ω * succ b ≤ a ^ ω * d
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
]

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this : a ^ ω * b + c ≤ a ^ ω * d
⊢ succ b ≤ d
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

Goal state before:
pp: case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * x + a * y

Tactic:
]

Goal state after:
case right
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d x : Ordinal.{u}
hx : x < b
hx' : c < a * x
y : Ordinal.{u}
hy : y < b
hy' : d < a * y
⊢ (fun x1 x2 ↦ x1 + x2) c d < a * x + a * y
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ (fun x1 x2 ↦ x1 * x2) a b ≤ 1

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ (fun x1 x2 ↦ x1 * x2) a b ≤ 1
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

Goal state before:
pp: case ind.mk.hbc.inr
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝¹ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this✝ : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : ℵ₀ ≤ #↑(Iio q)
this : #↑(Iio q) < #α
⊢ #↑(Iio q) < #α

Tactic:
]

Goal state after:
case ind.mk.hbc.inr
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝¹ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this✝ : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : ℵ₀ ≤ #↑(Iio q)
this : #↑(Iio q) < #α
⊢ #↑(Iio q) < #α
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
]

Goal state after:
case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ b < d
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

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 * c

Tactic:
]

Goal state after:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a ≤ c
hb : b ≤ c
⊢ a * b ≤ c * c
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
exact isNormal_preAleph.le_iff_forall_le ⟨by simpa, l⟩

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

Goal state before:
pp: a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}), deriv (fun x ↦ a * x) a_1 = a ^ ω * a_1 → deriv (fun x ↦ a * x) (succ a_1) = a ^ ω * succ a_1

Tactic:
]

Goal state after:
a : Ordinal.{u}
ha : 0 < a
⊢ deriv (fun x ↦ a * x) ⊥ = a ^ ω * ⊥ ∧
    ∀ (a_1 : Ordinal.{u}), deriv (fun x ↦ a * x) a_1 = a ^ ω * a_1 → deriv (fun x ↦ a * x) (succ a_1) = a ^ ω * succ a_1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

Goal state after:
case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b < c
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:
apply (mul_le_mul' (le_max_left a b) (le_max_right a b)).trans_lt
  obtain h | h := lt_or_ge (max a b) ℵ₀
  · exact (mul_lt_aleph0 h h).trans_le hc
  · rw [mul_eq_self h]
    exact max_lt ha hb

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

Goal state before:
pp: case refine_1
a : Ordinal.{u}
ha : 0 < a
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ max a b = max a b

pp: case e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b

Tactic:
]

Goal state after:
case e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ max a b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2

Tactic:
]

Goal state after:
case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ≤ a * b

Tactic:
]

Goal state after:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a ≤ a * b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case e'_3
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
h' : b ≠ 0
hb : b < ℵ₀
this : b ≤ a
⊢ a = a

Tactic:
]

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

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ nfp (fun x ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c

Tactic:
]

Goal state after:
case refine_2
a : Ordinal.{u}
ha : 0 < a
c : Ordinal.{u}
h : deriv (fun x ↦ a * x) c = a ^ ω * c
⊢ nfp (fun x ↦ a * x) (succ (a ^ ω * c)) = a ^ ω * succ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
h' : a ≠ 0
h : ℵ₀ ≤ b
⊢ b * a = max b a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 0 < a

Tactic:
]

Goal state after:
case a
o : Ordinal.{u}
h : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 0 < a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preAleph (ω + (o + 1)) = preAleph (ω + (o + 1))

Tactic:
]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω ≤ ω + o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
⊢ ω ≤ ω + o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α)) = Cardinal.lift.{u, max u v} (Order.cof (ULift.{v, u} α))

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
⊢ IsSuccLimit (ℵ_ o).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
]

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

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

pp: c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ preAleph.symm c
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ 0 < o

Tactic:
]

Goal state after:
case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ 0 < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2.inl
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
⊢ (fun x1 x2 ↦ x1 * x2) 0 b < o

Tactic:
dsimp only; rwa [zero_mul]

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

Goal state before:
pp: case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) ↔ ∃ x, IsMax x

Tactic:
]

Goal state after:
case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) ↔ ∃ x, IsMax x
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

Goal state before:
pp: case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀

Tactic:
]

Goal state after:
case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x1 x2 ↦ x1 * x2) a b < o

Tactic:
]

Goal state after:
case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x1 x2 ↦ x1 * x2) a b < o
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x1 x2 ↦ x1 * x2) a b < a * o

Tactic:
]

Goal state after:
case refine_2.inr
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun x1 x2 ↦ x1 * x2) a b < a * o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o < ω_ 1
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
⊢ Uncountable α ↔ Uncountable α

Tactic:
]

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

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

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀

Tactic:
]

Goal state after:
case inr.inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ max a b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Countable ↔ s.Countable

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r r)

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ Nonempty ((fun x1 x2 ↦ x1 < x2) ↪r r)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
⊢ ∃ i, preBeth a < 2 ^ preBeth ↑i

Tactic:
]

Goal state after:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ i, preBeth a < 2 ^ preBeth ↑i
Module: Mathlib.SetTheory.Ordinal.Principal

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

Tactic:
]

Goal state after:
case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ⨆ a, 2 ^ preBeth ↑a = 0

Tactic:
]

Goal state after:
⊢ ⨆ a, 2 ^ preBeth ↑a = 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

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
⊢ b = b

Tactic:
]

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

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

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
⊢ ⨆ a, 2 ^ preBeth ↑a = 2 ^ preBeth o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ ⨆ a, 2 ^ preBeth ↑a = ⨆ a, preBeth ↑a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * (n * b) < ω ^ c * ω

Tactic:
]

Goal state after:
case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ ω ^ c * (n * b) < ω ^ c * ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ ∀ (i : ↑(Iio o)), 2 ^ preBeth ↑i ≤ ⨆ x, preBeth ↑x

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ ∀ (i : ↑(Iio o)), 2 ^ preBeth ↑i ≤ ⨆ x, preBeth ↑x
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
h : b ≠ 0
⊢ a ≤ b * a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : ↑(Iio o)
⊢ preBeth (↑a + 1) ≤ ⨆ x, preBeth ↑x

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : ↑(Iio o)
⊢ preBeth (↑a + 1) ≤ ⨆ x, preBeth ↑x
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ StrictMono preBeth ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a

Tactic:
]

Goal state after:
⊢ StrictMono preBeth ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
⊢ a * b = a ↔ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
]

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ ∃ t ⊆ s, IsCofinal t ∧ typeLT ↑t = (Order.cof α).ord
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c

Tactic:
]

Goal state after:
case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
⊢ ∀ (i : ↑(Iio ω)), preBeth ↑i ≤ ℵ₀

Tactic:
]

Goal state after:
case a
⊢ ∀ (i : ↑(Iio ω)), preBeth ↑i ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
n : ℕ
ha : ↑n ∈ Iio ω
⊢ ↑((fun x ↦ 2 ^ x)^[n] 0) ≤ ℵ₀

Tactic:
]

Goal state after:
case a
n : ℕ
ha : ↑n ∈ Iio ω
⊢ ↑((fun x ↦ 2 ^ x)^[n] 0) ≤ ℵ₀