no goals
α : Type u_4
M : Type u_2
N : Type ?u.300771
P : Type ?u.300774
R : Type u_1
S : Type ?u.300780
inst✝¹² : Semiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
α' : Type ?u.300872
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v✝ : α → M
v' : α' → M'
f : M →ₗ[R] M'
v : α → M
l : α →₀ R
⊢ ↑f (↑(Finsupp.total α M R v) l) = ↑(Finsupp.total α M' R (↑f ∘ v)) l
apply Finsupp.induction_linear l <;> simp (config := { contextual := true })