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

State before:
R✝¹ : Type ?u.194642
inst✝³⁶ : Semiring R✝¹
X✝¹ : Type ?u.194648
inst✝³⁵ : TopologicalSpace X✝¹
inst✝³⁴ : AddCommMonoid X✝¹
inst✝³³ : Module R✝¹ X✝¹
Y✝¹ : Type ?u.194682
inst✝³² : TopologicalSpace Y✝¹
inst✝³¹ : AddCommMonoid Y✝¹
inst✝³⁰ : Module R✝¹ Y✝¹
R✝ : Type ?u.194714
inst✝²⁹ : Semiring R✝
X✝ : Type ?u.194720
inst✝²⁸ : TopologicalSpace X✝
inst✝²⁷ : AddCommMonoid X✝
inst✝²⁶ : Module R✝ X✝
Y✝ : Type ?u.194754
inst✝²⁵ : TopologicalSpace Y✝
inst✝²⁴ : AddCommMonoid Y✝
inst✝²³ : Module R✝ Y✝
Z✝ : Type ?u.194786
inst✝²² : TopologicalSpace Z✝
inst✝²¹ : AddCommMonoid Z✝
inst✝²⁰ : Module R✝ Z✝
ι✝ : Type ?u.194818
inst✝¹⁹ : Fintype ι✝
E✝ : ι✝ → Type ?u.194826
inst✝¹⁸ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝¹⁷ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝¹⁶ : (i : ι✝) → Module R✝ (E✝ i)
R : Type u_1
inst✝¹⁵ : Semiring R
X : Type u_3
inst✝¹⁴ : TopologicalSpace X
inst✝¹³ : AddCommMonoid X
inst✝¹² : Module R X
Y : Type u_2
inst✝¹¹ : TopologicalSpace Y
inst✝¹⁰ : AddCommMonoid Y
inst✝⁹ : Module R Y
Z : Type ?u.194950
inst✝⁸ : TopologicalSpace Z
inst✝⁷ : AddCommMonoid Z
inst✝⁶ : Module R Z
ι : Type ?u.194983
inst✝⁵ : Fintype ι
E : ι → Type ?u.194991
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : (i : ι) → AddCommMonoid (E i)
inst✝² : (i : ι) → Module R (E i)
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R Y
f : X → R
hf : IsContinuousLinearMap R f
y : Y
⊢ ∀ (x : X), f x • y = (ContinuousLinearMap.smulRight (mk' R f hf) y) x
Tactic:
simp
State after:
no goals