-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem mul_eq_opow_log_succ (ha : a ≠ 0) (hb : Principal (· * ·) b) (hb₂ : 2 < b) :
    a * b = b ^ succ (log b a)

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)

Tactic:
exact lt_opow_succ_log_self hb₁ _

Result:
no goals

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
⊢ a * b ≤ b ^ succ (log b a)

Tactic:
rw [← (isNormal_mul_right (Ordinal.pos_iff_ne_zero.2 ha)).bsup_eq hbl, bsup_le_iff]

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
⊢ ∀ i < b, a * i ≤ b ^ succ (log b a)

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
⊢ ∀ i < b, a * i ≤ b ^ succ (log b a)

Tactic:
intro c hcb

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
⊢ a * c ≤ b ^ succ (log b a)

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b

Tactic:
refine mul_le_mul_left' (hb (hbl.succ_lt ?_) hcb).le _

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
⊢ a * c ≤ b ^ succ (log b a)

Tactic:
have hbo₀ : b ^ log b a ≠ 0 := Ordinal.pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * c ≤ b ^ succ (log b a)

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)

Tactic:
have hbl := isLimit_of_principal_mul hb₂ hb

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
⊢ a * b ≤ b ^ succ (log b a)

Proof state:
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
⊢ a * b = b ^ succ (log b a)

Tactic:
apply le_antisymm

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
⊢ a * b ≤ b ^ succ (log b a)

case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a / b ^ log b a < b

Tactic:
rw [div_lt hbo₀, ← opow_succ]

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
⊢ a * c ≤ b ^ succ (log b a)

Tactic:
have hb₁ : 1 < b := one_lt_two.trans hb₂

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
⊢ a * c ≤ b ^ succ (log b a)

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * c ≤ b ^ succ (log b a)

Tactic:
apply (mul_le_mul_right' (le_of_lt (lt_mul_succ_div a hbo₀)) c).trans

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
⊢ b ^ log b a * b ≤ a * b

Tactic:
exact mul_le_mul_right' (opow_log_le_self b ha) b

Result:
no goals

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)

Tactic:
rw [mul_assoc, opow_succ]

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
hbl : b.IsLimit
c : Ordinal.{u}
hcb : c < b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b

Proof state:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
⊢ b ^ succ (log b a) ≤ a * b

Tactic:
rw [opow_succ]

Result:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : Principal (fun x1 x2 => x1 * x2) b
hb₂ : 2 < b
⊢ b ^ log b a * b ≤ a * b