case inl
G : Type ?u.140761
M✝ : Type ?u.140764
N : Type ?u.140767
α : Sort ?u.140770
β : Sort ?u.140773
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
⊢ (∑ᶠ (i : ι), f i) • 0 = ∑ᶠ (i : ι), f i • 0

case inr
G : Type ?u.140761
M✝ : Type ?u.140764
N : Type ?u.140767
α : Sort ?u.140770
β : Sort ?u.140773
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
hx : x ≠ 0
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
G : Type ?u.140761
M✝ : Type ?u.140764
N : Type ?u.140767
α : Sort ?u.140770
β : Sort ?u.140773
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
rcases eq_or_ne x 0 with (rfl | hx)
no goals
case inr
G : Type ?u.140761
M✝ : Type ?u.140764
N : Type ?u.140767
α : Sort ?u.140770
β : Sort ?u.140773
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
hx : x ≠ 0
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _
no goals
case inl
G : Type ?u.140761
M✝ : Type ?u.140764
N : Type ?u.140767
α : Sort ?u.140770
β : Sort ?u.140773
ι : Sort u_3
inst✝⁵ : CommMonoid M✝
inst✝⁴ : CommMonoid N
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
⊢ (∑ᶠ (i : ι), f i) • 0 = ∑ᶠ (i : ι), f i • 0
simp