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

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
<;>

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
<;>

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
⊢ (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
a b : Ordinal.{u_1}
h✝ : a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

pp: case neg
a b : Ordinal.{u_1}
h✝ : ¬a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
<;>

Goal state after:
case pos
a b : Ordinal.{u_1}
h✝ : a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝ : ¬a = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.blsub fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
<;>

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.blsub fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

pp: case neg
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

pp: case pos
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

pp: case neg
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

Tactic:
<;>

Goal state after:
case pos
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝¹ : a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case pos
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0

case neg
a b : Ordinal.{u_1}
h✝¹ : ¬a = 0
h✝ : ¬b = 0
⊢ a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case e'_2
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = (x * y + 0) % (x * z)

pp: case e'_3
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z) + 0

Tactic:
<;>

Goal state after:
case e'_2
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = (x * y + 0) % (x * z)

case e'_3
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z) + 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ^ b = 1 ↔ a = 1 ∨ b = 0

Tactic:
refine ⟨fun h ↦ ?_, by simp +contextual [or_imp]⟩

Goal state after:
a b : Ordinal.{u_1}
h : a ^ b = 1
⊢ a = 1 ∨ b = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : c = 0
⊢ a ^ c ≤ b ^ c

pp: case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : ¬c = 0
⊢ a ^ c ≤ b ^ c

Tactic:
<;>

Goal state after:
case pos
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : c = 0
⊢ a ^ c ≤ b ^ c

case neg
a b c : Ordinal.{u_1}
ab : a ≤ b
ha : a = 0
h✝ : ¬c = 0
⊢ a ^ c ≤ b ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

pp: case neg
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

Tactic:
<;>

Goal state after:
case pos
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c

case neg
b c : Ordinal.{u_1}
hb : 0 < b
this : b ≠ 0
h✝ : ¬c = 0
⊢ 0 ^ (b * c) = (0 ^ b) ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∈ Iic x
⊢ sSup univ = 0

pp: case neg
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∉ Iic x
⊢ sSup ∅ = 0

Tactic:
<;>

Goal state after:
case pos
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∈ Iic x
⊢ sSup univ = 0

case neg
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∉ Iic x
⊢ sSup ∅ = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b x c : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
⊢ 0 ∈ (fun x ↦ b ^ x) ⁻¹' Iic x

Tactic:
simpa [one_le_iff_ne_zero]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ n + b - 1 < succ 1 * b

pp: case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 < b

Tactic:
<;>

Goal state after:
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ n + b - 1 < succ 1 * b

case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ 0 < b
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i_1, f i (List.foldr f a i_1) ≤ ⨆ i, List.foldr f a i

pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i, List.foldr f a i ≤ ⨆ i_1, f i (List.foldr f a i_1)

Tactic:
<;>

Goal state after:
case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i_1, f i (List.foldr f a i_1) ≤ ⨆ i, List.foldr f a i

case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
⊢ ⨆ i, List.foldr f a i ≤ ⨆ i_1, f i (List.foldr f a i_1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inl
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 0 ≤ 1
⊢ 0 ^ log 0 x ≤ x

pp: case inl.inr
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 1 ≤ 1
⊢ 1 ^ log 1 x ≤ x

Tactic:
<;>

Goal state after:
case inl.inl
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 0 ≤ 1
⊢ 0 ^ log 0 x ≤ x

case inl.inr
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 1 ≤ 1
⊢ 1 ^ log 1 x ≤ x
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ b ^ log b x ≤ x

Tactic:
· rw [opow_le_iff_le_log hb hx]

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

Goal state before:
pp: b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y ↔ b ^ y ≤ x ∧ x < b ^ (y + 1)

Tactic:
constructor
  · rintro rfl
    use opow_log_le_self b hx, lt_opow_succ_log_self hb x
  · rintro ⟨hx₁, hx₂⟩
    apply le_antisymm
    · rwa [← lt_add_one_iff, ← lt_opow_iff_log_lt hb hx]
    · rwa [← opow_le_iff_le_log hb hx]

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

Goal state before:
pp: case mp
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap op) o → IsPrincipal op o

pp: case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal op o → IsPrincipal (Function.swap op) o

Tactic:
<;>

Goal state after:
case mp
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap op) o → IsPrincipal op o

case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal op o → IsPrincipal (Function.swap op) o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ↑n + 1 ≤ ↑(n + 1)

pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a ≠ 0

Tactic:
<;>

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ↑n + 1 ≤ ↑(n + 1)

case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a ≠ 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 0
⊢ a + o = o

pp: case refine_1.inr.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 1
⊢ a + o = o

Tactic:
<;>

Goal state after:
case refine_1.inr.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 0
⊢ a + o = o

case refine_1.inr.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h✝ : o = 1
⊢ a + o = o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

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

Tactic:
rw [← mul_eq_right_iff_opow_omega0_dvd]

Goal state after:
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl.inr
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
hb : b ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ b)

Tactic:
zero_opow hb

Goal state after:
case inl.inr
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
hb : b ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)) → x ∈ range fun a ↦ preBeth ↑a

pp: case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun a ↦ preBeth ↑a) → x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)

Tactic:
<;>

Goal state after:
case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)) → x ∈ range fun a ↦ preBeth ↑a

case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun a ↦ preBeth ↑a) → x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
b : Ordinal.{u}
hb✝ : b ∈ Iio (⨆ i, f i + 1)
hb : ∃ i, b ≤ f i
⊢ ∃ y ∈ range fun i ↦ ⟨f i, ⋯⟩, ⟨b, hb✝⟩ ≤ y

Tactic:
obtain ⟨i, hi⟩ := hb

Goal state after:
case refine_2.refine_1
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this : StrictMono fun i ↦ ⟨f i, ⋯⟩
b : Ordinal.{u}
hb : b ∈ Iio (⨆ i, f i + 1)
i : β
hi : b ≤ f i
⊢ ∃ y ∈ range fun i ↦ ⟨f i, ⋯⟩, ⟨b, hb⟩ ≤ y
Module: Mathlib.SetTheory.Ordinal.Principal

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

Tactic:
rw [← mul_assoc, mul_omega0 a0 ha]

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

Goal state before:
pp: case ha
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u, v} #β < (lift.{v, u} a.ord).cof

pp: case hf
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ ∀ (i : β), (f i).ord < a.ord

Tactic:
<;>

Goal state after:
case ha
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u, v} #β < (lift.{v, u} a.ord).cof

case hf
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ ∀ (i : β), (f i).ord < a.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case ha
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ #α < a.ord.cof

pp: case hf
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ∀ (i : α), (f i).ord < a.ord

Tactic:
<;>

Goal state after:
case ha
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ #α < a.ord.cof

case hf
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ∀ (i : α), (f i).ord < a.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a

Tactic:
rw [← ord_lt_ord, iSup_ord]
  apply Ordinal.iSup_lt_of_lt_cof <;> simpa

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

Goal state before:
pp: o : Ordinal.{u}
⊢ o.cof = sInf {a | ∃ ι f, lsub f = o ∧ #ι = a}

Tactic:
refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)

Goal state after:
case refine_1
o : Ordinal.{u}
⊢ ∀ b ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}, o.cof ≤ b

case refine_2
o : Ordinal.{u}
⊢ o.cof ∈ {a | ∃ ι f, lsub f = o ∧ #ι = a}
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ β ≠ α
⊢ β + γ ≤ α + γ ∧ β + γ ≠ α + γ

Tactic:
Ne

Goal state after:
α β γ : Cardinal.{u_1}
γ₀ : γ < ℵ₀
h : β ≤ α ∧ ¬β = α
⊢ β + γ ≤ α + γ ∧ ¬β + γ = α + γ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case mp
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c → a < b

pp: case mpr
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a < b → a + c < b + c

Tactic:
<;>

Goal state after:
case mp
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c → a < b

case mpr
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a < b → a + c < b + c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case mp
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b ≤ a → b + c ≤ a + c

pp: case mpr
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b + c ≤ a + c → b ≤ a

Tactic:
<;>

Goal state after:
case mp
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b ≤ a → b + c ≤ a + c

case mpr
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ b + c ≤ a + c → b ≤ a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ ∃ ι f, lsub f = o ∧ #ι = o.cof

Tactic:
rw [cof_eq_sInf_lsub]
  exact csInf_mem (cof_lsub_def_nonempty o)

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

Goal state before:
pp: case inl.refine_1
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < κ₂ + μ₂

pp: case inl.refine_2
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < κ₂ + μ₂

Tactic:
<;>

Goal state after:
case inl.refine_1
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < κ₂ + μ₂

case inl.refine_2
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < κ₂ + μ₂
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < ?inl.refine_1.b

pp: case inl.refine_1.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ ?inl.refine_1.b ≤ κ₂ + μ₂

pp: case inl.refine_1.b
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ Cardinal.{u_1}

pp: case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < ?inl.refine_2.b

pp: case inl.refine_2.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ ?inl.refine_2.b ≤ κ₂ + μ₂

pp: case inl.refine_2.b
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ Cardinal.{u_1}

Tactic:
<;>

Goal state after:
case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₁ < ?inl.refine_1.b

case inl.refine_1.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ ?inl.refine_1.b ≤ κ₂ + μ₂

case inl.refine_1.b
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ Cardinal.{u_1}

case hab
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₁ < ?inl.refine_2.b

case inl.refine_2.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ ?inl.refine_2.b ≤ κ₂ + μ₂

case inl.refine_2.b
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ Cardinal.{u_1}
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r (hrr'.toEmbedding ((enum r') ⟨i, x✝¹⟩)) (hrr'.toEmbedding ((enum r') ⟨j, h⟩))

Tactic:
hrr'.2,

Goal state after:
case refine_2
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
i j : Ordinal.{u}
x✝¹ : i < type r'
h : j < type r'
x✝ : i < j
⊢ r' ((enum r') ⟨i, x✝¹⟩) ((enum r') ⟨j, h⟩)
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl.inl
n m : ℕ
⊢ (↑n ^ ↑m).card ≤ max ℵ₀ (max (↑n).card (↑m).card)

Tactic:
rw [opow_natCast, ← natCast_pow, card_nat]
      exact le_max_of_le_left natCast_le_aleph0

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

Goal state before:
pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a.card ≤ (a ^ b).card

pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b.card ≤ (a ^ b).card

Tactic:
<;>

Goal state after:
a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ a.card ≤ (a ^ b).card

a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ b.card ≤ (a ^ b).card
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a.card ≤ (a ^ b).card

pp: a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b.card ≤ (a ^ b).card

Tactic:
<;>

Goal state after:
a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ a.card ≤ (a ^ b).card

a b : Ordinal.{u_1}
ha : 1 < a
hb : ω ≤ b
⊢ b.card ≤ (a ^ b).card
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_1.h₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} ℵ₀ < c.cof

pp: case h₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} #ι < c.cof

Tactic:
<;>

Goal state after:
case refine_1.h₁
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} ℵ₀ < c.cof

case h₂
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Ordinal.{max u v}
hc : ℵ₀ < c.cof
hc' : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), ∀ b < c, f i b < c
a : Ordinal.{max u v}
ha : a < c
⊢ Cardinal.lift.{v, u} #ι < c.cof
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_3
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i // ∀ (j : ι), r j i → f j < f i } → { i // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun i ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun i ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i // ∀ (j : ι), r j i → f j < f i } r'
⊢ a ≤ (type r').blsub fun i x ↦ f ↑((enum r') ⟨i, x⟩)

Tactic:
· rw [← hf, lsub_le_iff]
    intro i
    suffices h : ∃ i' hi', f i ≤ bfamilyOfFamily' r' (fun i => f i) i' hi' by
      rcases h with ⟨i', hi', hfg⟩
      exact hfg.trans_lt (lt_blsub _ _ _)
    by_cases! h : ∀ j, r j i → f j < f i
    · refine ⟨typein r' ⟨i, h⟩, typein_lt_type _ _, ?_⟩
      rw [bfamilyOfFamily'_typein]
    · obtain ⟨hji, hij⟩ := wo.wf.min_mem _ h
      refine ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le ?_ hij⟩, typein_lt_type _ _, ?_⟩
      · by_contra! H
        exact (wo.wf.not_lt_min {j | r j i ∧ f i ≤ f j} ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj
      · rwa [bfamilyOfFamily'_typein]

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

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) ≤ lift.{v, u} (2 ^ #ι)

Tactic:
refine (prod_le_prod _ _ h₂).trans_eq ?_
    rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]

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

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ lift.{v, u} 2 ≤ lift.{u, v} (c i)

Tactic:
rw [lift_two, ← lift_two.{u, v}, lift_le]

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ c i