Theorem: SciLean.IsContinuousLinearMap.HAdd.hAdd.arg_a0a1.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝¹ : Type ?u.100515
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.100521
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.100555
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
R✝ : Type ?u.100587
inst✝²⁸ : Semiring R✝
X✝ : Type ?u.100593
inst✝²⁷ : TopologicalSpace X✝
inst✝²⁶ : AddCommMonoid X✝
inst✝²⁵ : Module R✝ X✝
Y✝ : Type ?u.100627
inst✝²⁴ : TopologicalSpace Y✝
inst✝²³ : AddCommMonoid Y✝
inst✝²² : Module R✝ Y✝
Z✝ : Type ?u.100659
inst✝²¹ : TopologicalSpace Z✝
inst✝²⁰ : AddCommMonoid Z✝
inst✝¹⁹ : Module R✝ Z✝
ι✝ : Type ?u.100691
inst✝¹⁸ : Fintype ι✝
E✝ : ι✝ → Type ?u.100699
inst✝¹⁷ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁶ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁵ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_2
inst✝¹⁴ : Semiring R
X : Type u_3
inst✝¹³ : TopologicalSpace X
inst✝¹² : AddCommMonoid X
inst✝¹¹ : Module R X
Y : Type u_1
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : AddCommMonoid Y
inst✝⁸ : Module R Y
Z : Type ?u.100823
inst✝⁷ : TopologicalSpace Z
inst✝⁶ : AddCommMonoid Z
inst✝⁵ : Module R Z
ι : Type ?u.100856
inst✝⁴ : Fintype ι
E : ι → Type ?u.100864
inst✝³ : (i : ι) → TopologicalSpace (E i)
inst✝² : (i : ι) → AddCommMonoid (E i)
inst✝¹ : (i : ι) → Module R (E i)
inst✝ : ContinuousAdd Y
f g : X → Y
hf : IsContinuousLinearMap R f
hg : IsContinuousLinearMap R g
⊢ ∀ (x : X), f x + g x = (Add.add (mk' R f hf) (mk' R g hg)) x
Tactic:
simp[ContinuousLinearMap.add]
State after:
no goals