case h
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
⊢ List.length (digits b n) = log b n + 1
n✝ b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ List.length (digits b n) = log b n + 1
induction' n using Nat.strong_induction_on with n IH
case h
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
case h
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
⊢ List.length (digits b n) = log b n + 1
rw [digits_eq_cons_digits_div hb hn, List.length]
case pos
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1

case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
case h
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
by_cases h : n / b = 0
case pos
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : n / b = 0
hb0 : b ≠ 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
case pos
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
have hb0 : b ≠ 0 := (Nat.succ_le_iff.1 hb).ne_bot
no goals
case pos
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : n / b = 0
hb0 : b ≠ 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
simp [h, log_eq_zero_iff, ← Nat.div_eq_zero_iff hb0.bot_lt]
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ 1 ≤ log b n
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ List.length (digits b (n / b)) + 1 = log b n + 1
rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ b ≤ n
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ 1 ≤ log b n
refine' Nat.succ_le_of_lt (log_pos hb _)
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
this : n / b < n
h : n < b
⊢ n / b = 0
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ b ≤ n
contrapose! h
no goals
case neg
n✝¹ b n✝ : ℕ
hb : 1 < b
hn✝ : n✝ ≠ 0
n : ℕ
IH : ∀ (m : ℕ), m < n → m ≠ 0 → List.length (digits b m) = log b m + 1
hn : n ≠ 0
this : n / b < n
h : n < b
⊢ n / b = 0
exact div_eq_of_lt h