b n : ℕ
⊢ log b n ≤ log b (n + 1)
b : ℕ
⊢ Monotone (log b)
refine' monotone_nat_of_le_succ fun n => _
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)

case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)
b n : ℕ
⊢ log b n ≤ log b (n + 1)
cases' le_or_lt b 1 with hb hb
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ log b (n + 1)
rw [log_of_left_le_one hb]
no goals
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ log b (n + 1)
exact zero_le _
no goals
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ log b (n + 1)
exact le_log_of_pow_le hb (pow_log_le_add_one _ _)