-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dvd_bmod_dot_sub_dot_bmod (m : Nat) (xs ys : IntList) :
    (m : Int) ∣ bmod_dot_sub_dot_bmod m xs ys

Proof state:
case cons.cons
m : Nat
x : Int
xs : List Int
ih : ∀ (ys : IntList), ((dot xs ys).bmod m - (bmod xs m).dot ys) % ↑m = 0
y : Int
ys : List Int
⊢ ((dot (x :: xs) (y :: ys)).bmod m - (bmod (x :: xs) m).dot (y :: ys)) % ↑m = 0

Tactic:
simp only [IntList.dot_cons₂, List.map_cons]

Result:
case cons.cons
m : Nat
x : Int
xs : List Int
ih : ∀ (ys : IntList), ((dot xs ys).bmod m - (bmod xs m).dot ys) % ↑m = 0
y : Int
ys : List Int
⊢ ((x * y + dot xs ys).bmod m - (x.bmod m * y + dot (List.map (fun x => x.bmod m) xs) ys)) % ↑m = 0

Proof state:
case cons.cons
m : Nat
x : Int
xs : List Int
ih : ∀ (ys : IntList), ((dot xs ys).bmod m - (bmod xs m).dot ys) % ↑m = 0
y : Int
ys : List Int
⊢ ((x * y + dot xs ys).bmod m - (x.bmod m * y + dot (List.map (fun x => x.bmod m) xs) ys)) % ↑m = 0

Tactic:
specialize ih ys

Result:
case cons.cons
m : Nat
x : Int
xs : List Int
y : Int
ys : List Int
ih : ((dot xs ys).bmod m - (bmod xs m).dot ys) % ↑m = 0
⊢ ((x * y + dot xs ys).bmod m - (x.bmod m * y + dot (List.map (fun x => x.bmod m) xs) ys)) % ↑m = 0

Proof state:
case nil
m : Nat
ys : IntList
⊢ ((dot [] ys).bmod m - (bmod [] m).dot ys) % ↑m = 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.nil
m : Nat
x : Int
xs : List Int
ih : ∀ (ys : IntList), ((dot xs ys).bmod m - (bmod xs m).dot ys) % ↑m = 0
⊢ ((dot (x :: xs) []).bmod m - (bmod (x :: xs) m).dot []) % ↑m = 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
m : Nat
x : Int
xs : List Int
y : Int
ys : List Int
ih : ((dot xs ys).bmod m - (bmod xs m).dot ys) % ↑m = 0
⊢ ((x * y + dot xs ys).bmod m - (x.bmod m * y + dot (List.map (fun x => x.bmod m) xs) ys)) % ↑m = 0

Tactic:
rw [Int.sub_emod, Int.bmod_emod] at ih

Result:
case cons.cons
m : Nat
x : Int
xs : List Int
y : Int
ys : List Int
ih : (dot xs ys % ↑m - (bmod xs m).dot ys % ↑m) % ↑m = 0
⊢ ((x * y + dot xs ys).bmod m - (x.bmod m * y + dot (List.map (fun x => x.bmod m) xs) ys)) % ↑m = 0

Proof state:
m : Nat
xs ys : IntList
⊢ ↑m ∣ bmod_dot_sub_dot_bmod m xs ys

Tactic:
dsimp [bmod_dot_sub_dot_bmod]

Result:
m : Nat
xs ys : IntList
⊢ ↑m ∣ (xs.dot ys).bmod m - (xs.bmod m).dot ys

Proof state:
case cons.cons
m : Nat
x : Int
xs : List Int
y : Int
ys : List Int
ih : (dot xs ys % ↑m - (bmod xs m).dot ys % ↑m) % ↑m = 0
⊢ ((x * y + dot xs ys).bmod m - (x.bmod m * y + dot (List.map (fun x => x.bmod m) xs) ys)) % ↑m = 0

Tactic:
rw [Int.sub_emod, Int.bmod_emod, Int.add_emod, Int.add_emod (Int.bmod x m * y),
  ← Int.sub_emod, ← Int.sub_sub, Int.sub_eq_add_neg, Int.sub_eq_add_neg,
  Int.add_assoc (x * y % m), Int.add_comm (IntList.dot _ _ % m), ← Int.add_assoc,
  Int.add_assoc, ← Int.sub_eq_add_neg, ← Int.sub_eq_add_neg, Int.add_emod, ih, Int.add_zero,
  Int.emod_emod, Int.mul_emod, Int.mul_emod (Int.bmod x m), Int.bmod_emod, Int.sub_self,
  Int.zero_emod]

Result:
no goals

Proof state:
case cons
m : Nat
x : Int
xs : List Int
ih : ∀ (ys : IntList), ((dot xs ys).bmod m - (bmod xs m).dot ys) % ↑m = 0
ys : IntList
⊢ ((dot (x :: xs) ys).bmod m - (bmod (x :: xs) m).dot ys) % ↑m = 0

Tactic:
cases ys with
| nil => simp
| cons y ys =>
  simp only [IntList.dot_cons₂, List.map_cons]
  specialize ih ys
  rw [Int.sub_emod, Int.bmod_emod] at ih
  rw [Int.sub_emod, Int.bmod_emod, Int.add_emod, Int.add_emod (Int.bmod x m * y),
    ← Int.sub_emod, ← Int.sub_sub, Int.sub_eq_add_neg, Int.sub_eq_add_neg,
    Int.add_assoc (x * y % m), Int.add_comm (IntList.dot _ _ % m), ← Int.add_assoc,
    Int.add_assoc, ← Int.sub_eq_add_neg, ← Int.sub_eq_add_neg, Int.add_emod, ih, Int.add_zero,
    Int.emod_emod, Int.mul_emod, Int.mul_emod (Int.bmod x m), Int.bmod_emod, Int.sub_self,
    Int.zero_emod]

Result:
no goals

Proof state:
m : Nat
xs ys : IntList
⊢ ((xs.dot ys).bmod m - (xs.bmod m).dot ys) % ↑m = 0

Tactic:
induction xs generalizing ys with
| nil => simp
| cons x xs ih =>
  cases ys with
  | nil => simp
  | cons y ys =>
    simp only [IntList.dot_cons₂, List.map_cons]
    specialize ih ys
    rw [Int.sub_emod, Int.bmod_emod] at ih
    rw [Int.sub_emod, Int.bmod_emod, Int.add_emod, Int.add_emod (Int.bmod x m * y),
      ← Int.sub_emod, ← Int.sub_sub, Int.sub_eq_add_neg, Int.sub_eq_add_neg,
      Int.add_assoc (x * y % m), Int.add_comm (IntList.dot _ _ % m), ← Int.add_assoc,
      Int.add_assoc, ← Int.sub_eq_add_neg, ← Int.sub_eq_add_neg, Int.add_emod, ih, Int.add_zero,
      Int.emod_emod, Int.mul_emod, Int.mul_emod (Int.bmod x m), Int.bmod_emod, Int.sub_self,
      Int.zero_emod]

Result:
no goals

Proof state:
m : Nat
xs ys : IntList
⊢ ↑m ∣ (xs.dot ys).bmod m - (xs.bmod m).dot ys

Tactic:
rw [Int.dvd_iff_emod_eq_zero]

Result:
m : Nat
xs ys : IntList
⊢ ((xs.dot ys).bmod m - (xs.bmod m).dot ys) % ↑m = 0