case nil
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD ↑k]

case cons
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD ↑k]
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
induction' L with d L ih
no goals
case nil
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
⊢ ofDigits b [] ≡ ofDigits b' [] [ZMOD ↑k]
rfl
case cons
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ↑d + b * ofDigits b L ≡ ↑d + b' * ofDigits b' L [ZMOD ↑k]
case cons
n : ℕ
b b' : ℤ
k : ℕ
h : b ≡ b' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [ZMOD ↑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' [ZMOD ↑k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [ZMOD ↑k]
⊢ ↑d + b * ofDigits b L ≡ ↑d + b' * ofDigits b' L [ZMOD ↑k]
dsimp [Int.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 [Int.add_emod, Int.mul_emod, 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 [Int.add_emod, Int.mul_emod]