-- Mathlib/Data/Nat/Digits.lean
theorem digits_base_pow_mul {b k m : ℕ} (hb : 1 < b) (hm : 0 < m) :
    digits b (b ^ k * m) = List.replicate k 0 ++ digits b m

Proof state:
case zero
b : ℕ
hb : 1 < b
m : ℕ
hm : 0 < m
⊢ b.digits (b ^ 0 * m) = List.replicate 0 0 ++ b.digits m

Tactic:
simp

Result:
no goals

Proof state:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
have h2 : m = m * b / b :=
  Nat.eq_div_of_mul_eq_left (not_eq_zero_of_lt hb) rfl

Result:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
h2 : m = m * b / b
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Proof state:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
have hmb : 0 < m * b := lt_mul_of_lt_of_one_lt' hm hb

Result:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Proof state:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits (b ^ (k + 1) * m) = b.digits (b ^ k * (m * b))

Tactic:
ring_nf

Result:
no goals

Proof state:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
rw [List.replicate_succ', List.append_assoc, List.singleton_append, ← h1, ← ih hmb]

Result:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits (b ^ (k + 1) * m) = b.digits (b ^ k * (m * b))

Proof state:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
let h1 := digits_def' hb hmb

Result:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Proof state:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h1 : b.digits (m * b) = m * b % b :: b.digits (m * b / b) := digits_def' hb hmb
h2 : m = m * b / b
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Tactic:
simp only [mul_mod_left, ← h2] at h1

Result:
case succ
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ}, 0 < m → b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
hmb : 0 < m * b
h2 : m = m * b / b
h1 : b.digits (m * b) = 0 :: b.digits m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m

Proof state:
b k m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m

Tactic:
induction k generalizing m with
| zero => simp
| succ k ih =>
  have hmb : 0 < m * b := lt_mul_of_lt_of_one_lt' hm hb
  let h1 := digits_def' hb hmb
  have h2 : m = m * b / b :=
    Nat.eq_div_of_mul_eq_left (not_eq_zero_of_lt hb) rfl
  simp only [mul_mod_left, ← h2] at h1
  rw [List.replicate_succ', List.append_assoc, List.singleton_append, ← h1, ← ih hmb]
  ring_nf

Result:
no goals