case h
ι : Type u_5
ι' : Type ?u.181637
R : Type u_1
R₂ : Type ?u.181643
K : Type ?u.181646
M : Type u_3
M' : Type ?u.181652
M'' : Type ?u.181655
V : Type u
V' : Type ?u.181660
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
R₁ : Type u_2
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_4
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), ↑f₁ (↑b i) = ↑f₂ (↑b i)
x : M
⊢ ↑f₁ x = ↑f₂ x
ι : Type u_5
ι' : Type ?u.181637
R : Type u_1
R₂ : Type ?u.181643
K : Type ?u.181646
M : Type u_3
M' : Type ?u.181652
M'' : Type ?u.181655
V : Type u
V' : Type ?u.181660
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
R₁ : Type u_2
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_4
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), ↑f₁ (↑b i) = ↑f₂ (↑b i)
⊢ f₁ = f₂
ext x
case h
ι : Type u_5
ι' : Type ?u.181637
R : Type u_1
R₂ : Type ?u.181643
K : Type ?u.181646
M : Type u_3
M' : Type ?u.181652
M'' : Type ?u.181655
V : Type u
V' : Type ?u.181660
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
R₁ : Type u_2
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_4
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), ↑f₁ (↑b i) = ↑f₂ (↑b i)
x : M
⊢ ↑f₁ (∑ a in (↑b.repr x).support, ↑(↑b.repr x) a • ↑b a) = ↑f₂ (∑ a in (↑b.repr x).support, ↑(↑b.repr x) a • ↑b a)
case h
ι : Type u_5
ι' : Type ?u.181637
R : Type u_1
R₂ : Type ?u.181643
K : Type ?u.181646
M : Type u_3
M' : Type ?u.181652
M'' : Type ?u.181655
V : Type u
V' : Type ?u.181660
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
R₁ : Type u_2
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_4
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), ↑f₁ (↑b i) = ↑f₂ (↑b i)
x : M
⊢ ↑f₁ x = ↑f₂ x
rw [← b.total_repr x, Finsupp.total_apply, Finsupp.sum]
no goals
case h
ι : Type u_5
ι' : Type ?u.181637
R : Type u_1
R₂ : Type ?u.181643
K : Type ?u.181646
M : Type u_3
M' : Type ?u.181652
M'' : Type ?u.181655
V : Type u
V' : Type ?u.181660
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
R₁ : Type u_2
inst✝⁴ : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
M₁ : Type u_4
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h : ∀ (i : ι), ↑f₁ (↑b i) = ↑f₂ (↑b i)
x : M
⊢ ↑f₁ (∑ a in (↑b.repr x).support, ↑(↑b.repr x) a • ↑b a) = ↑f₂ (∑ a in (↑b.repr x).support, ↑(↑b.repr x) a • ↑b a)
simp only [LinearMap.map_sum, LinearMap.map_smulₛₗ, h]