case h
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_2
inst✝¹⁵ : Ring R₂
R₃ : Type u_3
inst✝¹⁴ : Ring R₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommGroup M
M₂ : Type u_4
inst✝¹¹ : TopologicalSpace M₂
inst✝¹⁰ : AddCommGroup M₂
M₃ : Type u_5
inst✝⁹ : TopologicalSpace M₃
inst✝⁸ : AddCommGroup M₃
M₄ : Type ?u.856610
inst✝⁷ : TopologicalSpace M₄
inst✝⁶ : AddCommGroup M₄
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : TopologicalAddGroup M₂
inst✝ : TopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
x✝ : M
⊢ ↑(comp g (f₁ - f₂)) x✝ = ↑(comp g f₁ - comp g f₂) x✝
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_2
inst✝¹⁵ : Ring R₂
R₃ : Type u_3
inst✝¹⁴ : Ring R₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommGroup M
M₂ : Type u_4
inst✝¹¹ : TopologicalSpace M₂
inst✝¹⁰ : AddCommGroup M₂
M₃ : Type u_5
inst✝⁹ : TopologicalSpace M₃
inst✝⁸ : AddCommGroup M₃
M₄ : Type ?u.856610
inst✝⁷ : TopologicalSpace M₄
inst✝⁶ : AddCommGroup M₄
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : TopologicalAddGroup M₂
inst✝ : TopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
⊢ comp g (f₁ - f₂) = comp g f₁ - comp g f₂
ext
no goals
case h
R : Type u_1
inst✝¹⁶ : Ring R
R₂ : Type u_2
inst✝¹⁵ : Ring R₂
R₃ : Type u_3
inst✝¹⁴ : Ring R₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommGroup M
M₂ : Type u_4
inst✝¹¹ : TopologicalSpace M₂
inst✝¹⁰ : AddCommGroup M₂
M₃ : Type u_5
inst✝⁹ : TopologicalSpace M₃
inst✝⁸ : AddCommGroup M₃
M₄ : Type ?u.856610
inst✝⁷ : TopologicalSpace M₄
inst✝⁶ : AddCommGroup M₄
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : TopologicalAddGroup M₂
inst✝ : TopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M →SL[σ₁₂] M₂
x✝ : M
⊢ ↑(comp g (f₁ - f₂)) x✝ = ↑(comp g f₁ - comp g f₂) x✝
simp