no goals
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
ys : List α
⊢ prod [] * prod ys =
    prod (zipWith (fun x x_1 => x * x_1) [] ys) * prod (drop (length ys) []) * prod (drop (length []) ys)
simp [Nat.zero_le]
no goals
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
xs : List α
⊢ prod xs * prod [] =
    prod (zipWith (fun x x_1 => x * x_1) xs []) * prod (drop (length []) xs) * prod (drop (length xs) [])
simp [Nat.zero_le]
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * prod xs * (y * prod ys) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ prod (x :: xs) * prod (y :: ys) =
    prod (zipWith (fun x x_1 => x * x_1) (x :: xs) (y :: ys)) * prod (drop (length (y :: ys)) (x :: xs)) *
      prod (drop (length (x :: xs)) (y :: ys))
simp only [drop, length, zipWith_cons_cons, prod_cons]
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * (y * (prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys))) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * prod xs * (y * prod ys) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
conv =>
  lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
  rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * (y * (prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys))) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys)
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * (y * (prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys))) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (Nat.add (length ys) 0) xs) *
      prod (drop (Nat.add (length xs) 0) ys)
simp only [add_eq, add_zero]
no goals
α : Type u
β : Type ?u.284124
γ : Type ?u.284127
δ : Type ?u.284130
ε : Type ?u.284133
inst✝ : CommMonoid α
x : α
xs : List α
y : α
ys : List α
⊢ x * (y * (prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys))) =
    x * y * prod (zipWith (fun x x_1 => x * x_1) xs ys) * prod (drop (length ys) xs) * prod (drop (length xs) ys)
ac_rfl