case h.e'_2
b : Ordinal
hb : 1 < b
x : Ordinal
⊢ log b (b ^ x) = log b (b ^ x * 1 + 0)
b : Ordinal
hb : 1 < b
x : Ordinal
⊢ log b (b ^ x) = x
convert log_opow_mul_add hb zero_ne_one.symm hb (opow_pos x (zero_lt_one.trans hb))
  using 1
no goals
case h.e'_2
b : Ordinal
hb : 1 < b
x : Ordinal
⊢ log b (b ^ x) = log b (b ^ x * 1 + 0)
rw [add_zero, mul_one]