b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ (if h : b ≤ n ∧ 1 < b then
      let_fun this := (_ : n / b < n);
      log b (n / b) + 1
    else 0) =
    log b (n / b) + 1
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n = log b (n / b) + 1
rw [log]
no goals
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ (if h : b ≤ n ∧ 1 < b then
      let_fun this := (_ : n / b < n);
      log b (n / b) + 1
    else 0) =
    log b (n / b) + 1
exact if_pos ⟨hn, h⟩