Theorem: SciLean.IsContinuousLinearMap.HSMul.hSMul.arg_a1.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝² : Type ?u.207940
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.207946
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.207980
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.208012
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.208018
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.208052
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.208084
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.208116
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.208124
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.208174
inst✝²¹ : Semiring R✝
X✝ : Type ?u.208180
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.208215
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.208248
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.208281
inst✝¹¹ : Fintype ι
E : ι → Type ?u.208289
inst✝¹⁰ : (i : ι) → TopologicalSpace (E i)
inst✝⁹ : (i : ι) → AddCommMonoid (E i)
inst✝⁸ : (i : ι) → Module R✝ (E i)
R : Type u_1
inst✝⁷ : CommSemiring 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
inst✝ : ContinuousConstSMul R Y
c : R
f : X → Y
hf : IsContinuousLinearMap R f
⊢ ∀ (x : X), c • f x = (ContinuousLinearMap.smulLeft (mk' R f hf) c) x
Tactic:
simp
State after:
no goals