no goals
𝕜 : Type u_6
inst✝¹⁶ : NontriviallyNormedField 𝕜
E : Type ?u.212501
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedSpace 𝕜 E
F : Type u_5
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace 𝕜 F
G : Type ?u.212686
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace 𝕜 G
R : Type u_1
𝕜₂ : Type u_7
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_3
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_4
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
x x' : M
y : F
⊢ ↑(↑f (x - x')) y = ↑(↑f x) y - ↑(↑f x') y
rw [f.map_sub, sub_apply]