case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n

case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
b n : ℕ
⊢ log b n ≤ clog b n
obtain hb | hb := le_or_lt b 1
no goals
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n
cases n with
| zero =>
  rw [log_zero_right]
  exact zero_le _
| succ n =>
  exact (pow_right_strictMono hb).le_iff_le.1
    ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n
rw [log_of_left_le_one hb]
no goals
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n
exact zero_le _
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b zero
case inr.zero
b : ℕ
hb : 1 < b
⊢ log b zero ≤ clog b zero
rw [log_zero_right]
no goals
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b zero
exact zero_le _
no goals
case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (succ n) ≤ clog b (succ n)
exact (pow_right_strictMono hb).le_iff_le.1
  ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)