case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b ↑Nat.zero = ↑(Nat.log b Nat.zero)

case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(Nat.succ n✝) = ↑(Nat.log b (Nat.succ n✝))
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ log b ↑n = ↑(Nat.log b n)
cases n
no goals
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ log b ↑Nat.zero = ↑(Nat.log b Nat.zero)
simp [log_of_right_le_one]
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(Nat.succ n✝)
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ log b ↑(Nat.succ n✝) = ↑(Nat.log b (Nat.succ n✝))
rw [log_of_one_le_right, Nat.floor_coe]
no goals
case succ.hr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n✝ : ℕ
⊢ 1 ≤ ↑(Nat.succ n✝)
simp