awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
inl : ∀ (h : o % b ^ log b o = 0), log b (o % b ^ log b o) < log b o
inr : ∀ (h : o % b ^ log b o ≠ 0), log b (o % b ^ log b o) < log b o
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h

Premises used: HMod.hMod, HPow.hPow, Ordinal.log, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
inl : 0 < log b o
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rw [h, log_zero_right]

Premises used: Ordinal.log_zero_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o

Tactic:
log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo

Premises used: LT.lt.le, Order.one_le_iff_ne_zero, Iff.mp, LE.le.trans, Ordinal.log_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o

Tactic:
exact log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo

Premises used: LT.lt.le, Order.one_le_iff_ne_zero, Iff.mp, LE.le.trans, Ordinal.log_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
inr : o % b ^ log b o < b ^ log b o
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rw [← lt_opow_iff_log_lt hb h]

Premises used: Ordinal.lt_opow_iff_log_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ o % b ^ log b o < b ^ log b o

Tactic:
mod_lt _ (opow_pos _ hb.pos).ne'

Premises used: LT.lt.pos, Ordinal.mod_lt, LT.lt.ne', Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ o % b ^ log b o < b ^ log b o

Tactic:
exact mod_lt _ (opow_pos _ hb.pos).ne'

Premises used: LT.lt.pos, Ordinal.mod_lt, LT.lt.ne', Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
mp : log b x = y → b ^ y ≤ x ∧ x < b ^ (y + 1)
mpr : b ^ y ≤ x ∧ x < b ^ (y + 1) → log b x = y
⊢ log b x = y ↔ b ^ y ≤ x ∧ x < b ^ (y + 1)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
left : b ^ log b x ≤ x
right : x < b ^ (log b x + 1)
⊢ b ^ log b x ≤ x ∧ x < b ^ (log b x + 1)

Tactic:
use opow_log_le_self b hx, lt_opow_succ_log_self hb x

Premises used: Ordinal.opow_log_le_self, Ordinal.lt_opow_succ_log_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
mpr : log b x ≤ y
mpr₁ : y ≤ log b x
⊢ log b x = y

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
mpr : log b x < y + 1
mpr₁ mpr₂ mpr₃ mpr₄ : x < b ^ (y + 1)
⊢ log b x ≤ y

Tactic:
rwa [← lt_add_one_iff, ← lt_opow_iff_log_lt hb hx]

Premises used: Order.lt_add_one_iff, Ordinal.lt_opow_iff_log_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
mpr mpr₁ mpr₂ mpr₃ : b ^ y ≤ x
⊢ y ≤ log b x

Tactic:
rwa [← opow_le_iff_le_log hb hx]

Premises used: Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
rw : b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)
hx : b ^ u * v + w ≠ 0
⊢ log b (b ^ u * v + w) = u + log b v

Tactic:
rw [log_eq_iff hb]

Premises used: Ordinal.log_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
left : b ^ (u + log b v) ≤ b ^ u * v + w
right : b ^ u * v + w < b ^ (u + log b v + 1)
⊢ b ^ (u + log b v) ≤ b ^ u * v + w ∧ b ^ u * v + w < b ^ (u + log b v + 1)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
left : b ^ u * b ^ log b v ≤ b ^ u * v + w
left₁ : b ^ u * v ≤ b ^ u * v + w
left₂ left₃ : b ^ u * v ≤ b ^ u * v
⊢ b ^ (u + log b v) ≤ b ^ u * v + w

Tactic:
grw [opow_add, opow_log_le_self b hv, ← le_self_add]

Premises used: Ordinal.opow_add, Ordinal.opow_log_le_self, le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
right : b ^ u * v + b ^ u ≤ b ^ (u + log b v + 1)
⊢ b ^ u * v + w < b ^ (u + log b v + 1)

Tactic:
apply (add_lt_add_right hw _).trans_le

Premises used: add_lt_add_right, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
right : b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)
⊢ b ^ u * v + b ^ u ≤ b ^ (u + log b v + 1)

Tactic:
rw [← mul_add_one, add_assoc, opow_add]

Premises used: Ordinal.opow_add, add_assoc, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
right : v + 1 ≤ b ^ (log b v + 1)
⊢ b ^ u * (v + 1) ≤ b ^ u * b ^ (log b v + 1)

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
right : v < b ^ (log b v + 1)
⊢ v + 1 ≤ b ^ (log b v + 1)

Tactic:
rw [add_one_le_iff]

Premises used: Order.add_one_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v < b ^ (log b v + 1)

Tactic:
lt_opow_succ_log_self hb _

Premises used: Order.succ, Ordinal.lt_opow_succ_log_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v < b ^ (log b v + 1)

Tactic:
exact lt_opow_succ_log_self hb _

Premises used: Ordinal.lt_opow_succ_log_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0

Tactic:
fun h ↦ mul_ne_zero (opow_ne_zero u (bot_lt_of_lt hb).ne') hv <|
      left_eq_zero_of_add_eq_zero h

Premises used: bot_lt_of_lt, Ordinal.left_eq_zero_of_add_eq_zero, Ordinal.opow_ne_zero, LT.lt.ne', mul_ne_zero, Not
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w ≠ 0

Tactic:
exact fun h ↦ mul_ne_zero (opow_ne_zero u (bot_lt_of_lt hb).ne') hv <|
      left_eq_zero_of_add_eq_zero h

Premises used: bot_lt_of_lt, Ordinal.left_eq_zero_of_add_eq_zero, Ordinal.opow_ne_zero, LT.lt.ne', mul_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b v : Ordinal.{u_1}
hb : 1 < b
u : Ordinal.{u_1}
hv : v ≠ 0
⊢ log b (b ^ u * v) = u + log b v

Tactic:
simpa using log_opow_mul_add hb hv (opow_pos u (bot_lt_of_lt hb))

Premises used: bot_lt_of_lt, Ordinal.log_opow_mul_add, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ log b (b ^ x * 1) = x + log b 1

Tactic:
log_opow_mul hb x zero_ne_one.symm

Premises used: Ordinal.log_opow_mul, zero_ne_one, Ne.symm
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
h : log b (b ^ x) = log b (b ^ x * 1)
h₁ : x = x + log b 1
⊢ log b (b ^ x) = x

Tactic:
convert! log_opow_mul hb x zero_ne_one.symm using 1

Premises used: Ordinal.log_opow_mul, zero_ne_one, Ne.symm
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
h h₁ : log b (b ^ x) = log b (b ^ x)
⊢ log b (b ^ x) = log b (b ^ x * 1)

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
h : x = x + 0
h₁ h₂ : x = x
⊢ x = x + log b 1

Tactic:
rw [log_one_right, add_zero]

Premises used: add_zero, Ordinal.log_one_right
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
inl : 0 < o / HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o)
inr : ∀ (hb : 0 < b), 0 < o / b ^ log b o
⊢ 0 < o / b ^ log b o

Tactic:
rcases eq_zero_or_pos b with (rfl | hb)

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / HPow.hPow (α := Ordinal.{u_1}) 0 (log 0 o)

Tactic:
simpa using pos_iff_ne_zero.2 ho

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
inr : b ^ log b o ≤ o
⊢ 0 < o / b ^ log b o

Tactic:
rw [div_pos (opow_ne_zero _ hb.ne')]

Premises used: Ordinal.opow_ne_zero, LT.lt.ne', Ordinal.div_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o

Tactic:
opow_log_le_self b ho

Premises used: Ordinal.opow_log_le_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : 0 < b
⊢ b ^ log b o ≤ o

Tactic:
exact opow_log_le_self b ho

Premises used: Ordinal.opow_log_le_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
rw : o < b ^ succ (log b o)
⊢ o / b ^ log b o < b

Tactic:
rw [← lt_mul_iff_div_lt (opow_pos _ (zero_lt_one.trans hb)).ne', ← opow_succ]

Premises used: Ordinal.lt_mul_iff_div_lt, LT.lt.ne', zero_lt_one, LT.lt.trans, Ordinal.opow_succ, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)

Tactic:
lt_opow_succ_log_self hb o

Premises used: Ordinal.lt_opow_succ_log_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
b o : Ordinal.{u_1}
hb : 1 < b
⊢ o < b ^ succ (log b o)

Tactic:
exact lt_opow_succ_log_self hb o

Premises used: Ordinal.lt_opow_succ_log_self
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
a : o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) ≤ 1
a₁ : 1 ≤ o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o)
⊢ o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) ≤ 1

Tactic:
simpa [← one_add_one_eq_two] using div_opow_log_lt o one_lt_two

Premises used: Ordinal.div_opow_log_lt, one_add_one_eq_two, one_lt_two
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 1 ≤ o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o)

Tactic:
simpa [one_le_iff_ne_zero, pos_iff_ne_zero] using div_opow_log_pos 2 ho

Premises used: Ordinal.div_opow_log_pos, Order.one_le_iff_ne_zero, OfNat.ofNat, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * (o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o)) +
      o % HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) =
    o

Tactic:
div_add_mod ..

Premises used: Ordinal.div_add_mod
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
h :
  HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) =
    HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * (o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o))
⊢ HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) + o % HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = o

Tactic:
convert! div_add_mod .. using 2

Premises used: Ordinal.div_add_mod
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
o : Ordinal.{u_1}
ho : o ≠ 0
h : HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * 1
h₁ h₂ : HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) = HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o)
⊢ HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) =
    HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o) * (o / HPow.hPow (α := Ordinal.{u_1}) 2 (log 2 o))

Tactic:
rw [div_two_opow_log ho, mul_one]

Premises used: Ordinal.div_two_opow_log, mul_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
inl : ∀ (hb : 1 < b), log b x + log b y ≤ log b (x * y)
inr : ∀ (hb : b ≤ 1), log b x + log b y ≤ log b (x * y)
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
obtain hb | hb := lt_or_ge 1 b

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
inl : b ^ log b x * b ^ log b y ≤ x * y
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]

Premises used: Ordinal.opow_add, mul_ne_zero, Ordinal.opow_le_iff_le_log
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y

Tactic:
mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)

Premises used: Ordinal.opow_log_le_self, mul_le_mul'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y

Tactic:
exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)

Premises used: Ordinal.opow_log_le_self, mul_le_mul'
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
simpa only [log_of_left_le_one hb, zero_add] using le_rfl

Premises used: Ordinal.log_of_left_le_one, le_rfl, zero_add
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
apply : ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ succ a
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ b

Tactic:
apply lt_of_lt_of_le _ (opow_le_opow_right omega0_pos (succ_le_of_lt h))

Premises used: Ordinal.opow_le_opow_right, Ordinal.omega0_pos, Order.succ_le_of_lt, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
rw : ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * ω
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ succ a

Tactic:
rw [opow_succ]

Premises used: Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
ha : 0 < ω ^ a
hbc : (↑n : Ordinal.{u_1}) < ω
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * ω

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ 0 < ω ^ a

Tactic:
opow_pos a omega0_pos

Premises used: Ordinal.omega0_pos, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ (↑n : Ordinal.{u_1}) < ω

Tactic:
natCast_lt_omega0 n

Premises used: Ordinal.natCast_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
h : a < b
n : ℕ
⊢ 0 < ω ^ a

Tactic:
exacts [opow_pos a omega0_pos, natCast_lt_omega0 n]

Premises used: Ordinal.omega0_pos, Ordinal.natCast_lt_omega0, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ a < ω ^ b ↔ ∃ c < b, ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})

Tactic:
⟨fun ha ↦ ⟨_, lt_log_of_lt_opow hb ha, ?_⟩,
    fun ⟨c, hc, n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt hc n)⟩

Premises used: Ordinal.omega0, Ordinal.lt_log_of_lt_opow, _private.0.Ordinal.lt_omega0_opow.match_1, HPow.hPow, Ordinal.log, And.intro, LT.lt, Iff.intro, Exists.intro, LT.lt.trans, Ordinal.omega0_opow_mul_nat_lt
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
refine : ∀ (ha : a < ω ^ b), ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})
⊢ a < ω ^ b ↔ ∃ c < b, ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})

Tactic:
refine ⟨fun ha ↦ ⟨_, lt_log_of_lt_opow hb ha, ?_⟩,
    fun ⟨c, hc, n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt hc n)⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
obtain : ∀ (n : ℕ) (hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})), ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})
⊢ ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})

Tactic:
obtain ⟨n, hn⟩ := lt_omega0.1 (div_opow_log_lt a one_lt_omega0)

Premises used: Ordinal.div_opow_log_lt, Iff.mp, Ordinal.lt_omega0, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})
h : a < ω ^ log ω a * (↑(n + 1) : Ordinal.{u_1})
⊢ ∃ (n : ℕ), a < ω ^ log ω a * (↑n : Ordinal.{u_1})

Tactic:
use n + 1
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})
h : a < ω ^ log ω a * (a / ω ^ log ω a + 1)
⊢ a < ω ^ log ω a * (↑(n + 1) : Ordinal.{u_1})

Tactic:
rw [Nat.cast_add_one, ← hn]

Premises used: Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})
⊢ a < ω ^ log ω a * (a / ω ^ log ω a + 1)

Tactic:
lt_mul_succ_div a (opow_ne_zero _ omega0_ne_zero)

Premises used: Order.succ, Ordinal.lt_mul_succ_div, Ordinal.opow_ne_zero, Ordinal.omega0_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
ha : a < ω ^ b
n : ℕ
hn : a / ω ^ log ω a = (↑n : Ordinal.{u_1})
⊢ a < ω ^ log ω a * (a / ω ^ log ω a + 1)

Tactic:
exact lt_mul_succ_div a (opow_ne_zero _ omega0_ne_zero)

Premises used: Ordinal.lt_mul_succ_div, Ordinal.opow_ne_zero, Ordinal.omega0_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
⊢ a < ω ^ succ b ↔ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})

Tactic:
⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt (lt_succ b) n)⟩

Premises used: Order.succ, Ordinal.omega0, Order.lt_succ, HPow.hPow, LT.lt, Iff.intro, LT.lt.trans, Ordinal.omega0_opow_mul_nat_lt, _private.0.Ordinal.lt_omega0_opow_succ.match_1
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
refine : ∀ (ha : a < ω ^ succ b), ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})
⊢ a < ω ^ succ b ↔ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})

Tactic:
refine ⟨fun ha ↦ ?_, fun ⟨n, hn⟩ ↦ hn.trans (omega0_opow_mul_nat_lt (lt_succ b) n)⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
obtain :
  ∀ (c : Ordinal.{u_1}) (hc : c < b + 1) (n : ℕ) (hn : a < ω ^ c * (↑n : Ordinal.{u_1})),
    ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})
⊢ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})

Tactic:
obtain ⟨c, hc, n, hn⟩ := (lt_omega0_opow (add_pos_of_right zero_lt_one b).ne').1 ha

Premises used: add_pos_of_right, LT.lt.ne', zero_lt_one, Ordinal.lt_omega0_opow, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * (↑n : Ordinal.{u_1})
⊢ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})

Tactic:
⟨n, hn.trans_le ?_⟩

Premises used: LT.lt.trans_le, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * (↑n : Ordinal.{u_1})
refine : ω ^ c * (↑n : Ordinal.{u_1}) ≤ ω ^ b * (↑n : Ordinal.{u_1})
⊢ ∃ (n : ℕ), a < ω ^ b * (↑n : Ordinal.{u_1})

Tactic:
refine ⟨n, hn.trans_le ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * (↑n : Ordinal.{u_1})
h₁ : 0 < ω
⊢ ω ^ c * (↑n : Ordinal.{u_1}) ≤ ω ^ b * (↑n : Ordinal.{u_1})

Tactic:
grw [lt_succ_iff.1 hc]

Premises used: Order.lt_succ_iff, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * (↑n : Ordinal.{u_1})
⊢ 0 < ω

Tactic:
omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
ha : a < ω ^ succ b
c : Ordinal.{u_1}
hc : c < b + 1
n : ℕ
hn : a < ω ^ c * (↑n : Ordinal.{u_1})
⊢ 0 < ω

Tactic:
exact omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
simp_rw :
  (∃ (c : Ordinal.{u_1}),
      (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) ↔
    ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
⊢ a < ω ^ ω ^ b ↔ ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))

Tactic:
simp_rw [lt_omega0_opow (opow_ne_zero _ omega0_ne_zero), lt_omega0_opow hb]

Premises used: Ordinal.opow_ne_zero, Ordinal.omega0_ne_zero, Ordinal.lt_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a b : Ordinal.{u_1}
hb : b ≠ 0
mp :
  (∃ (c : Ordinal.{u_1}),
      (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) →
    ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))
mpr :
  (∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))) →
    ∃ (c : Ordinal.{u_1}),
      (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})
⊢ (∃ (c : Ordinal.{u_1}),
      (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a < ω ^ c * (↑n : Ordinal.{u_1})) ↔
    ∃ c < b, ∃ (n : ℕ), a < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a_1 b_1 : Ordinal.{u_1}
hb_1 : b_1 ≠ 0
a b : Ordinal.{u_1}
hb : b < b_1
m : ℕ
hm : a < ω ^ b * (↑m : Ordinal.{u_1})
n : ℕ
hn : a_1 < ω ^ a * (↑n : Ordinal.{u_1})
⊢ ∃ c < b_1, ∃ (n : ℕ), a_1 < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))

Tactic:
⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩

Premises used: Iff.mpr, mul_le_mul_right, Nat.le_succ, Ordinal.natCast_lt_omega0, LT.lt.trans_le, And.intro, Exists.intro, LT.lt.trans, Ordinal.opow_mul_lt_opow, Nat.cast_le
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a_1 b_1 : Ordinal.{u_1}
hb_1 : b_1 ≠ 0
a b : Ordinal.{u_1}
hb : b < b_1
m : ℕ
hm : a < ω ^ b * (↑m : Ordinal.{u_1})
n : ℕ
hn : a_1 < ω ^ a * (↑n : Ordinal.{u_1})
⊢ ∃ c < b_1, ∃ (n : ℕ), a_1 < ω ^ (ω ^ c * (↑n : Ordinal.{u_1}))

Tactic:
exact ⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a_1 b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1}))
⊢ ∃ (c : Ordinal.{u_1}),
    (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a_1 < ω ^ c * (↑n : Ordinal.{u_1})

Tactic:
⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩

Premises used: HMul.hMul, Ordinal.omega0, Nat.cast, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a_1 b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1}))
mpr : ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * (↑(n + 1) : Ordinal.{u_1})
mpr₁ : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1})) * (↑1 : Ordinal.{u_1})
⊢ ∃ (c : Ordinal.{u_1}),
    (∃ c_1 < b, ∃ (n : ℕ), c < ω ^ c_1 * (↑n : Ordinal.{u_1})) ∧ ∃ (n : ℕ), a_1 < ω ^ c * (↑n : Ordinal.{u_1})

Tactic:
refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a_1 b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1}))
⊢ ω ^ a * (↑n : Ordinal.{u_1}) < ω ^ a * (↑(n + 1) : Ordinal.{u_1})

Tactic:
simp [mul_lt_mul_iff_right₀, opow_pos]

Premises used: mul_lt_mul_iff_right₀, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
a_1 b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1}))
⊢ a_1 < ω ^ (ω ^ a * (↑n : Ordinal.{u_1})) * (↑1 : Ordinal.{u_1})

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m : ℕ
⊢ (↑(HPow.hPow (β := ℕ) m 0) : Ordinal.{u_1}) = HPow.hPow (α := Ordinal.{u_1}) (β := ℕ) (↑m : Ordinal.{u_1}) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Exponential
Goal:
m n : ℕ
⊢ (↑(m ^ (n + 1)) : Ordinal.{u_1}) = HPow.hPow (α := Ordinal.{u_1}) (↑m : Ordinal.{u_1}) (n + 1)

Tactic:
simp [pow_succ, natCast_pow m n]

Premises used: pow_succ