R✝ : Type ?u.3532
R₁ : Type ?u.3535
R₂ : Type ?u.3538
R₃ : Type ?u.3541
R₄ : Type ?u.3544
S : Type ?u.3547
K : Type ?u.3550
K₂ : Type ?u.3553
M✝ : Type ?u.3556
M' : Type ?u.3559
M₁ : Type ?u.3562
M₂✝ : Type ?u.3565
M₃ : Type ?u.3568
M₄ : Type ?u.3571
N : Type ?u.3574
N₂ : Type ?u.3577
ι : Type ?u.3580
V : Type ?u.3583
V₂ : Type ?u.3586
α : Type u_1
R : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ (sum v fun i c_1 => ↑(h i) (c • c_1)) = sum v fun a b => c • ↑(h a) b

R✝ : Type ?u.3532
R₁ : Type ?u.3535
R₂ : Type ?u.3538
R₃ : Type ?u.3541
R₄ : Type ?u.3544
S : Type ?u.3547
K : Type ?u.3550
K₂ : Type ?u.3553
M✝ : Type ?u.3556
M' : Type ?u.3559
M₁ : Type ?u.3562
M₂✝ : Type ?u.3565
M₃ : Type ?u.3568
M₄ : Type ?u.3571
N : Type ?u.3574
N₂ : Type ?u.3577
ι : Type ?u.3580
V : Type ?u.3583
V₂ : Type ?u.3586
α : Type u_1
R : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ ∀ (i : α), ↑(h i) 0 = 0
R✝ : Type ?u.3532
R₁ : Type ?u.3535
R₂ : Type ?u.3538
R₃ : Type ?u.3541
R₄ : Type ?u.3544
S : Type ?u.3547
K : Type ?u.3550
K₂ : Type ?u.3553
M✝ : Type ?u.3556
M' : Type ?u.3559
M₁ : Type ?u.3562
M₂✝ : Type ?u.3565
M₃ : Type ?u.3568
M₄ : Type ?u.3571
N : Type ?u.3574
N₂ : Type ?u.3577
ι : Type ?u.3580
V : Type ?u.3583
V₂ : Type ?u.3586
α : Type u_1
R : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ (sum (c • v) fun a => ↑(h a)) = c • sum v fun a => ↑(h a)
rw [Finsupp.sum_smul_index', Finsupp.smul_sum]
no goals
R✝ : Type ?u.3532
R₁ : Type ?u.3535
R₂ : Type ?u.3538
R₃ : Type ?u.3541
R₄ : Type ?u.3544
S : Type ?u.3547
K : Type ?u.3550
K₂ : Type ?u.3553
M✝ : Type ?u.3556
M' : Type ?u.3559
M₁ : Type ?u.3562
M₂✝ : Type ?u.3565
M₃ : Type ?u.3568
M₄ : Type ?u.3571
N : Type ?u.3574
N₂ : Type ?u.3577
ι : Type ?u.3580
V : Type ?u.3583
V₂ : Type ?u.3586
α : Type u_1
R : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ (sum v fun i c_1 => ↑(h i) (c • c_1)) = sum v fun a b => c • ↑(h a) b
simp only [map_smul]
R✝ : Type ?u.3532
R₁ : Type ?u.3535
R₂ : Type ?u.3538
R₃ : Type ?u.3541
R₄ : Type ?u.3544
S : Type ?u.3547
K : Type ?u.3550
K₂ : Type ?u.3553
M✝ : Type ?u.3556
M' : Type ?u.3559
M₁ : Type ?u.3562
M₂✝ : Type ?u.3565
M₃ : Type ?u.3568
M₄ : Type ?u.3571
N : Type ?u.3574
N₂ : Type ?u.3577
ι : Type ?u.3580
V : Type ?u.3583
V₂ : Type ?u.3586
α : Type u_1
R : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
i : α
⊢ ↑(h i) 0 = 0
R✝ : Type ?u.3532
R₁ : Type ?u.3535
R₂ : Type ?u.3538
R₃ : Type ?u.3541
R₄ : Type ?u.3544
S : Type ?u.3547
K : Type ?u.3550
K₂ : Type ?u.3553
M✝ : Type ?u.3556
M' : Type ?u.3559
M₁ : Type ?u.3562
M₂✝ : Type ?u.3565
M₃ : Type ?u.3568
M₄ : Type ?u.3571
N : Type ?u.3574
N₂ : Type ?u.3577
ι : Type ?u.3580
V : Type ?u.3583
V₂ : Type ?u.3586
α : Type u_1
R : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
⊢ ∀ (i : α), ↑(h i) 0 = 0
intro i
no goals
R✝ : Type ?u.3532
R₁ : Type ?u.3535
R₂ : Type ?u.3538
R₃ : Type ?u.3541
R₄ : Type ?u.3544
S : Type ?u.3547
K : Type ?u.3550
K₂ : Type ?u.3553
M✝ : Type ?u.3556
M' : Type ?u.3559
M₁ : Type ?u.3562
M₂✝ : Type ?u.3565
M₃ : Type ?u.3568
M₄ : Type ?u.3571
N : Type ?u.3574
N₂ : Type ?u.3577
ι : Type ?u.3580
V : Type ?u.3583
V₂ : Type ?u.3586
α : Type u_1
R : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
v : α →₀ M
c : R
h : α → M →ₗ[R] M₂
i : α
⊢ ↑(h i) 0 = 0
exact (h i).map_zero