case h.e'_2
ι : Type u'
ι' : Type ?u.19688
R : Type u_1
K : Type ?u.19694
M : Type u_2
M' : Type ?u.19700
M'' : Type ?u.19703
V : Type u
V' : Type ?u.19708
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
H : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0
ι : Type u'
ι' : Type ?u.19688
R : Type u_1
K : Type ?u.19694
M : Type u_2
M' : Type ?u.19700
M'' : Type ?u.19703
V : Type u
V' : Type ?u.19708
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
H : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = 0
convert
  H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
    (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) i
no goals
case h.e'_2
ι : Type u'
ι' : Type ?u.19688
R : Type u_1
K : Type ?u.19694
M : Type u_2
M' : Type ?u.19700
M'' : Type ?u.19703
V : Type u
V' : Type ?u.19708
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
H : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0
exact (if_pos hi).symm
no goals
ι : Type u'
ι' : Type ?u.19688
R : Type u_1
K : Type ?u.19694
M : Type u_2
M' : Type ?u.19700
M'' : Type ?u.19703
V : Type u
V' : Type ?u.19708
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
H : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ i in s, (fun j => if j ∈ s then g j else 0) i • v i = 0
simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]