case nil
n b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]

case cons
n b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]
n b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [MOD k]
induction' L with d L ih
no goals
case nil
n b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]
rfl
case cons
n b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]
case cons
n b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]
dsimp [ofDigits]
case cons
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k
case cons
n b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]
dsimp [Nat.ModEq] at *
case cons
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
case cons
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k
conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]
no goals
case cons
n b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k
conv_rhs => rw [Nat.add_mod, Nat.mul_mod]