α : Type u
β : Type ?u.290919
γ : Type ?u.290922
δ : Type ?u.290925
ε : Type ?u.290928
inst✝ : CommMonoid α
L L' : List α
h : length L = length L'
⊢ prod (zipWith (fun x x_1 => x * x_1) L L') * prod (drop (length L') L) * prod (drop (length L) L') =
    prod (zipWith (fun x x_1 => x * x_1) L L')
α : Type u
β : Type ?u.290919
γ : Type ?u.290922
δ : Type ?u.290925
ε : Type ?u.290928
inst✝ : CommMonoid α
L L' : List α
h : length L = length L'
⊢ prod L * prod L' = prod (zipWith (fun x x_1 => x * x_1) L L')
apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop L L').trans
no goals
α : Type u
β : Type ?u.290919
γ : Type ?u.290922
δ : Type ?u.290925
ε : Type ?u.290928
inst✝ : CommMonoid α
L L' : List α
h : length L = length L'
⊢ prod (zipWith (fun x x_1 => x * x_1) L L') * prod (drop (length L') L) * prod (drop (length L) L') =
    prod (zipWith (fun x x_1 => x * x_1) L L')
rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]