-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_sdiv_left (xs ys : IntList) {d : Int} (h : d ∣ xs.gcd) :
    dot (xs.sdiv d) ys = (dot xs ys) / d

Proof state:
case cons.cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
y : Int
ys : List Int
wx : d ∣ x
⊢ (sdiv (x :: xs) d).dot (y :: ys) = dot (x :: xs) (y :: ys) / d

Tactic:
have wxy : d ∣ x * y := Int.dvd_trans wx (Int.dvd_mul_right x y)

Result:
case cons.cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
y : Int
ys : List Int
wx : d ∣ x
wxy : d ∣ x * y
⊢ (sdiv (x :: xs) d).dot (y :: ys) = dot (x :: xs) (y :: ys) / d

Proof state:
case cons.nil
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
⊢ (sdiv (x :: xs) d).dot [] = dot (x :: xs) [] / d

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
y : Int
ys : List Int
⊢ (sdiv (x :: xs) d).dot (y :: ys) = dot (x :: xs) (y :: ys) / d

Tactic:
have wx : d ∣ x := Int.dvd_trans h (gcd_cons_div_left)

Result:
case cons.cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
y : Int
ys : List Int
wx : d ∣ x
⊢ (sdiv (x :: xs) d).dot (y :: ys) = dot (x :: xs) (y :: ys) / d

Proof state:
case cons.cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
y : Int
ys : List Int
wx : d ∣ x
wxy : d ∣ x * y
⊢ (sdiv (x :: xs) d).dot (y :: ys) = dot (x :: xs) (y :: ys) / d

Tactic:
have w : d ∣ (IntList.gcd xs : Int) := Int.dvd_trans h (gcd_cons_div_right')

Result:
case cons.cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
y : Int
ys : List Int
wx : d ∣ x
wxy : d ∣ x * y
w : d ∣ ↑(gcd xs)
⊢ (sdiv (x :: xs) d).dot (y :: ys) = dot (x :: xs) (y :: ys) / d

Proof state:
case cons.cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
h : d ∣ ↑(gcd (x :: xs))
y : Int
ys : List Int
wx : d ∣ x
wxy : d ∣ x * y
w : d ∣ ↑(gcd xs)
⊢ (sdiv (x :: xs) d).dot (y :: ys) = dot (x :: xs) (y :: ys) / d

Tactic:
simp_all [Int.add_ediv_of_dvd_left, Int.mul_ediv_assoc']

Result:
no goals

Proof state:
case nil
d : Int
ys : IntList
h : d ∣ ↑(gcd [])
⊢ (sdiv [] d).dot ys = dot [] ys / d

Tactic:
simp

Result:
no goals

Proof state:
case cons
d x : Int
xs : List Int
ih : ∀ (ys : IntList), d ∣ ↑(gcd xs) → (sdiv xs d).dot ys = dot xs ys / d
ys : IntList
h : d ∣ ↑(gcd (x :: xs))
⊢ (sdiv (x :: xs) d).dot ys = dot (x :: xs) ys / d

Tactic:
cases ys with
| nil => simp
| cons y ys =>
  have wx : d ∣ x := Int.dvd_trans h (gcd_cons_div_left)
  have wxy : d ∣ x * y := Int.dvd_trans wx (Int.dvd_mul_right x y)
  have w : d ∣ (IntList.gcd xs : Int) := Int.dvd_trans h (gcd_cons_div_right')
  simp_all [Int.add_ediv_of_dvd_left, Int.mul_ediv_assoc']

Result:
no goals

Proof state:
xs ys : IntList
d : Int
h : d ∣ ↑xs.gcd
⊢ (xs.sdiv d).dot ys = xs.dot ys / d

Tactic:
induction xs generalizing ys with
| nil => simp
| cons x xs ih =>
  cases ys with
  | nil => simp
  | cons y ys =>
    have wx : d ∣ x := Int.dvd_trans h (gcd_cons_div_left)
    have wxy : d ∣ x * y := Int.dvd_trans wx (Int.dvd_mul_right x y)
    have w : d ∣ (IntList.gcd xs : Int) := Int.dvd_trans h (gcd_cons_div_right')
    simp_all [Int.add_ediv_of_dvd_left, Int.mul_ediv_assoc']

Result:
no goals