Theorem: SciLean.IsContinuousLinearMap.HSub.hSub.arg_a0a1.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝² : Type ?u.111801
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.111807
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.111841
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.111873
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.111879
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.111913
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.111945
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.111977
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.111985
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.112035
inst✝²¹ : Semiring R✝
X✝ : Type ?u.112041
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.112076
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.112109
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.112142
inst✝¹¹ : Fintype ι
E : ι → Type ?u.112150
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommMonoid (E i)
inst✝⁸ : (i : ι) → Module R✝ (E i)
R : Type u_1
inst✝⁷ : Ring R
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : AddCommGroup X
inst✝⁴ : Module R X
Y : Type u_3
inst✝³ : TopologicalSpace Y
inst✝² : AddCommGroup Y
inst✝¹ : Module R Y
inst✝ : TopologicalAddGroup Y
f g : X → Y
hf : IsContinuousLinearMap R f
hg : IsContinuousLinearMap R g
⊢ ∀ (x : X), f x - g x = (Sub.sub (mk' R f hf) (mk' R g hg)) x
Tactic:
simp[ContinuousLinearMap.sub]
State after:
no goals