case h
ι : Type u_4
ι' : Type u_3
R : Type u_1
R₂ : Type ?u.370286
K : Type ?u.370289
M : Type u_2
M' : Type ?u.370295
M'' : Type ?u.370298
V : Type u
V' : Type ?u.370303
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ : M
b' : Basis ι' R M'
e : ι ≃ ι'
x : M
⊢ ↑(sumCoords (reindex b e)) x = ↑(sumCoords b) x
ι : Type u_4
ι' : Type u_3
R : Type u_1
R₂ : Type ?u.370286
K : Type ?u.370289
M : Type u_2
M' : Type ?u.370295
M'' : Type ?u.370298
V : Type u
V' : Type ?u.370303
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ sumCoords (reindex b e) = sumCoords b
ext x
case h
ι : Type u_4
ι' : Type u_3
R : Type u_1
R₂ : Type ?u.370286
K : Type ?u.370289
M : Type u_2
M' : Type ?u.370295
M'' : Type ?u.370298
V : Type u
V' : Type ?u.370303
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ : M
b' : Basis ι' R M'
e : ι ≃ ι'
x : M
⊢ (Finsupp.sum (Finsupp.mapDomain (↑e) (↑b.repr x)) fun x => id) = Finsupp.sum (↑b.repr x) fun x => id
case h
ι : Type u_4
ι' : Type u_3
R : Type u_1
R₂ : Type ?u.370286
K : Type ?u.370289
M : Type u_2
M' : Type ?u.370295
M'' : Type ?u.370298
V : Type u
V' : Type ?u.370303
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ : M
b' : Basis ι' R M'
e : ι ≃ ι'
x : M
⊢ ↑(sumCoords (reindex b e)) x = ↑(sumCoords b) x
simp only [coe_sumCoords, repr_reindex]
no goals
case h
ι : Type u_4
ι' : Type u_3
R : Type u_1
R₂ : Type ?u.370286
K : Type ?u.370289
M : Type u_2
M' : Type ?u.370295
M'' : Type ?u.370298
V : Type u
V' : Type ?u.370303
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x✝ : M
b' : Basis ι' R M'
e : ι ≃ ι'
x : M
⊢ (Finsupp.sum (Finsupp.mapDomain (↑e) (↑b.repr x)) fun x => id) = Finsupp.sum (↑b.repr x) fun x => id
exact Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl