ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
⊢ ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • (w • v) i = 0 → ∀ (i : ι), g i = 0
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : LinearIndependent R v
w : ι → G
⊢ LinearIndependent R (w • v)
rw [linearIndependent_iff''] at hv⊢
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ g i = 0
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
⊢ ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • (w • v) i = 0 → ∀ (i : ι), g i = 0
intro s g hgs hsum i
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ w i • g i = 0
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ g i = 0
refine' (smul_eq_zero_iff_eq (w i)).1 _
case refine'_1
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ (fun i => w i • g i) i = 0

case refine'_2
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∑ i in s, (fun i => w i • g i) i • v i = 0
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ w i • g i = 0
refine' hv s (fun i => w i • g i) (fun i hi => _) _ i
case refine'_1
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ w i • g i = 0
case refine'_1
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ (fun i => w i • g i) i = 0
dsimp only
no goals
case refine'_1
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i✝ i : ι
hi : ¬i ∈ s
⊢ w i • g i = 0
exact (hgs i hi).symm ▸ smul_zero _
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∀ (x : ι), x ∈ s → (fun i => w i • g i) x • v x = g x • (w • v) x
case refine'_2
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∑ i in s, (fun i => w i • g i) i • v i = 0
rw [← hsum, Finset.sum_congr rfl _]
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i x✝ : ι
a✝ : x✝ ∈ s
⊢ (fun i => w i • g i) x✝ • v x✝ = g x✝ • (w • v) x✝
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i : ι
⊢ ∀ (x : ι), x ∈ s → (fun i => w i • g i) x • v x = g x • (w • v) x
intros
no goals
ι : Type u'
ι' : Type ?u.270528
R : Type u_2
K : Type ?u.270534
M : Type u_3
M' : Type ?u.270540
M'' : Type ?u.270543
V : Type u
V' : Type ?u.270548
v✝ : ι → M
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup M'
inst✝⁷ : AddCommGroup M''
inst✝⁶ : Module R M
inst✝⁵ : Module R M'
inst✝⁴ : Module R M''
a b : R
x y : M
G : Type u_1
hG : Group G
inst✝³ : DistribMulAction G R
inst✝² : DistribMulAction G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv : ∀ (s : Finset ι) (g : ι → R), (∀ (i : ι), ¬i ∈ s → g i = 0) → ∑ i in s, g i • v i = 0 → ∀ (i : ι), g i = 0
w : ι → G
s : Finset ι
g : ι → R
hgs : ∀ (i : ι), ¬i ∈ s → g i = 0
hsum : ∑ i in s, g i • (w • v) i = 0
i x✝ : ι
a✝ : x✝ ∈ s
⊢ (fun i => w i • g i) x✝ • v x✝ = g x✝ • (w • v) x✝
erw [Pi.smul_apply, smul_assoc, smul_comm]