case nil
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l'✝ : List β
f : α → β → γ
n : γ
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) [] l') = n * sum (zipWith f [] l')

case cons
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l'✝ : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) l') = n * sum (zipWith f (hd :: tl) l')
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f : α → β → γ
n : γ
l : List α
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) l l') = n * sum (zipWith f l l')
induction' l with hd tl hl generalizing f n l'
no goals
case nil
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l'✝ : List β
f : α → β → γ
n : γ
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) [] l') = n * sum (zipWith f [] l')
simp
case cons.nil
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l' : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) []) = n * sum (zipWith f (hd :: tl) [])

case cons.cons
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l' : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
hd' : β
tl' : List β
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) (hd' :: tl')) = n * sum (zipWith f (hd :: tl) (hd' :: tl'))
case cons
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l'✝ : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
l' : List β
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) l') = n * sum (zipWith f (hd :: tl) l')
cases' l' with hd' tl'
no goals
case cons.nil
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l' : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) []) = n * sum (zipWith f (hd :: tl) [])
simp
no goals
case cons.cons
α : Type u
β : Type u_2
γ✝ : Type ?u.177919
δ : Type ?u.177922
ε : Type ?u.177925
γ : Type u_1
inst✝ : Semiring γ
f✝ : α → β → γ
n✝ : γ
l' : List β
hd : α
tl : List α
hl : ∀ (f : α → β → γ) (n : γ) (l' : List β), sum (zipWith (fun x y => n * f x y) tl l') = n * sum (zipWith f tl l')
f : α → β → γ
n : γ
hd' : β
tl' : List β
⊢ sum (zipWith (fun x y => n * f x y) (hd :: tl) (hd' :: tl')) = n * sum (zipWith f (hd :: tl) (hd' :: tl'))
simp [hl, mul_add]