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