Theorem: SciLean.IsContinuousLinearMap.comp_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝ : Type ?u.25843
inst✝²⁰ : Semiring R✝
X✝ : Type ?u.25849
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R✝ X✝
Y✝ : Type ?u.25883
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R✝ Y✝
R : Type u_1
inst✝¹³ : Semiring R
X : Type u_2
inst✝¹² : TopologicalSpace X
inst✝¹¹ : AddCommMonoid X
inst✝¹⁰ : Module R X
Y : Type u_3
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : AddCommMonoid Y
inst✝⁷ : Module R Y
Z : Type u_4
inst✝⁶ : TopologicalSpace Z
inst✝⁵ : AddCommMonoid Z
inst✝⁴ : Module R Z
ι : Type ?u.26019
inst✝³ : Fintype ι
E : ι → Type ?u.26027
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
g : X → Y
hg : IsContinuousLinearMap R g
f : Y → Z
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), f (g x) = (ContinuousLinearMap.comp (mk' R f hf) (mk' R g hg)) x
Tactic:
simp[ContinuousLinearMap.comp]
State after:
no goals