α : Type u_1
M : Type u_3
N : Type ?u.394504
P : Type ?u.394507
R : Type u_2
S : Type ?u.394513
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.394605
M' : Type ?u.394608
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v✝ : α → M
v' : α' → M'
v : Option α → M
f : Option α →₀ R
⊢ (↑f none • v none + sum (some f) fun a r => r • v (Option.some a)) =
    ↑f none • v none + sum (some f) fun i a => a • (v ∘ Option.some) i
α : Type u_1
M : Type u_3
N : Type ?u.394504
P : Type ?u.394507
R : Type u_2
S : Type ?u.394513
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.394605
M' : Type ?u.394608
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v✝ : α → M
v' : α' → M'
v : Option α → M
f : Option α →₀ R
⊢ ↑(Finsupp.total (Option α) M R v) f = ↑f none • v none + ↑(Finsupp.total α M R (v ∘ Option.some)) (some f)
rw [total_apply, sum_option_index_smul, total_apply]
no goals
α : Type u_1
M : Type u_3
N : Type ?u.394504
P : Type ?u.394507
R : Type u_2
S : Type ?u.394513
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.394605
M' : Type ?u.394608
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M
inst✝¹ : Module R M'
inst✝ : Module R M
v✝ : α → M
v' : α' → M'
v : Option α → M
f : Option α →₀ R
⊢ (↑f none • v none + sum (some f) fun a r => r • v (Option.some a)) =
    ↑f none • v none + sum (some f) fun i a => a • (v ∘ Option.some) i
simp