-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_set_left (xs ys : IntList) (i : Nat) (z : Int) :
    dot (xs.set i z) ys = dot xs ys + (z - xs.get i) * ys.get i

Proof state:
case nil.succ
z : Int
i : Nat
a✝ : ∀ (ys : IntList), (set [] i z).dot ys = dot [] ys + (z - get [] i) * ys.get i
ys : IntList
⊢ (set [] (i + 1) z).dot ys = dot [] ys + (z - get [] (i + 1)) * ys.get (i + 1)

Tactic:
cases ys <;> simp_all

Result:
no goals

Proof state:
case cons.zero.cons
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
y : Int
ys : List Int
⊢ (set (x :: xs) 0 z).dot (y :: ys) = dot (x :: xs) (y :: ys) + (z - get (x :: xs) 0) * get (y :: ys) 0

Tactic:
simp only [Nat.zero_eq, set_cons_zero, dot_cons₂, get_cons_zero, Int.sub_mul]

Result:
case cons.zero.cons
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
y : Int
ys : List Int
⊢ z * y + dot xs ys = x * y + dot xs ys + (z * y - x * y)

Proof state:
case cons.zero.cons
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
y : Int
ys : List Int
⊢ z * y + dot xs ys = x * y + dot xs ys + (z * y - x * y)

Tactic:
rw [Int.add_right_comm, Int.add_comm (x * y), Int.sub_add_cancel]

Result:
no goals

Proof state:
case cons.zero
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
ys : IntList
⊢ (set (x :: xs) 0 z).dot ys = dot (x :: xs) ys + (z - get (x :: xs) 0) * ys.get 0

Tactic:
cases ys with
| nil => simp
| cons y ys =>
  simp only [Nat.zero_eq, set_cons_zero, dot_cons₂, get_cons_zero, Int.sub_mul]
  rw [Int.add_right_comm, Int.add_comm (x * y), Int.sub_add_cancel]

Result:
no goals

Proof state:
case cons.succ.nil
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
i : Nat
a✝ : ∀ (ys : IntList), (set (x :: xs) i z).dot ys = dot (x :: xs) ys + (z - get (x :: xs) i) * ys.get i
⊢ (set (x :: xs) (i + 1) z).dot [] = dot (x :: xs) [] + (z - get (x :: xs) (i + 1)) * get [] (i + 1)

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.cons
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
i : Nat
a✝ : ∀ (ys : IntList), (set (x :: xs) i z).dot ys = dot (x :: xs) ys + (z - get (x :: xs) i) * ys.get i
y : Int
ys : List Int
⊢ (set (x :: xs) (i + 1) z).dot (y :: ys) =
    dot (x :: xs) (y :: ys) + (z - get (x :: xs) (i + 1)) * get (y :: ys) (i + 1)

Tactic:
simp_all [Int.add_assoc]

Result:
no goals

Proof state:
case nil.zero
z : Int
ys : IntList
⊢ (set [] 0 z).dot ys = dot [] ys + (z - get [] 0) * ys.get 0

Tactic:
cases ys <;> simp

Result:
no goals

Proof state:
case nil
z : Int
ys : IntList
i : Nat
⊢ (set [] i z).dot ys = dot [] ys + (z - get [] i) * ys.get i

Tactic:
induction i generalizing ys with
| zero => cases ys <;> simp
| succ i => cases ys <;> simp_all

Result:
no goals

Proof state:
case cons.zero.nil
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
⊢ (set (x :: xs) 0 z).dot [] = dot (x :: xs) [] + (z - get (x :: xs) 0) * get [] 0

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
i : Nat
a✝ : ∀ (ys : IntList), (set (x :: xs) i z).dot ys = dot (x :: xs) ys + (z - get (x :: xs) i) * ys.get i
ys : IntList
⊢ (set (x :: xs) (i + 1) z).dot ys = dot (x :: xs) ys + (z - get (x :: xs) (i + 1)) * ys.get (i + 1)

Tactic:
cases ys with
| nil => simp
| cons y ys => simp_all [Int.add_assoc]

Result:
no goals

Proof state:
case cons
z x : Int
xs : List Int
ih : ∀ (ys : IntList) (i : Nat), (set xs i z).dot ys = dot xs ys + (z - get xs i) * ys.get i
ys : IntList
i : Nat
⊢ (set (x :: xs) i z).dot ys = dot (x :: xs) ys + (z - get (x :: xs) i) * ys.get i

Tactic:
induction i generalizing ys with
| zero =>
  cases ys with
  | nil => simp
  | cons y ys =>
    simp only [Nat.zero_eq, set_cons_zero, dot_cons₂, get_cons_zero, Int.sub_mul]
    rw [Int.add_right_comm, Int.add_comm (x * y), Int.sub_add_cancel]
| succ i =>
  cases ys with
  | nil => simp
  | cons y ys => simp_all [Int.add_assoc]

Result:
no goals

Proof state:
xs ys : IntList
i : Nat
z : Int
⊢ (xs.set i z).dot ys = xs.dot ys + (z - xs.get i) * ys.get i

Tactic:
induction xs generalizing i ys with
| nil =>
  induction i generalizing ys with
  | zero => cases ys <;> simp
  | succ i => cases ys <;> simp_all
| cons x xs ih =>
  induction i generalizing ys with
  | zero =>
    cases ys with
    | nil => simp
    | cons y ys =>
      simp only [Nat.zero_eq, set_cons_zero, dot_cons₂, get_cons_zero, Int.sub_mul]
      rw [Int.add_right_comm, Int.add_comm (x * y), Int.sub_add_cancel]
  | succ i =>
    cases ys with
    | nil => simp
    | cons y ys => simp_all [Int.add_assoc]

Result:
no goals