Theorem: SciLean.IsContinuousLinearMap.HMul.hMul.arg_a1.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝² : Type ?u.167279
inst✝⁴² : Semiring R✝²
X✝² : Type ?u.167285
inst✝⁴¹ : TopologicalSpace X✝²
inst✝⁴⁰ : AddCommMonoid X✝²
inst✝³⁹ : Module R✝² X✝²
Y✝² : Type ?u.167319
inst✝³⁸ : TopologicalSpace Y✝²
inst✝³⁷ : AddCommMonoid Y✝²
inst✝³⁶ : Module R✝² Y✝²
R✝¹ : Type ?u.167351
inst✝³⁵ : Semiring R✝¹
X✝¹ : Type ?u.167357
inst✝³⁴ : TopologicalSpace X✝¹
inst✝³³ : AddCommMonoid X✝¹
inst✝³² : Module R✝¹ X✝¹
Y✝¹ : Type ?u.167391
inst✝³¹ : TopologicalSpace Y✝¹
inst✝³⁰ : AddCommMonoid Y✝¹
inst✝²⁹ : Module R✝¹ Y✝¹
Z✝ : Type ?u.167423
inst✝²⁸ : TopologicalSpace Z✝
inst✝²⁷ : AddCommMonoid Z✝
inst✝²⁶ : Module R✝¹ Z✝
ι✝ : Type ?u.167455
inst✝²⁵ : Fintype ι✝
E✝ : ι✝ → Type ?u.167463
inst✝²⁴ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²³ : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²² : (i : ι✝) → Module R✝¹ (E✝ i)
R✝ : Type ?u.167513
inst✝²¹ : Semiring R✝
X✝ : Type ?u.167519
inst✝²⁰ : TopologicalSpace X✝
inst✝¹⁹ : AddCommMonoid X✝
inst✝¹⁸ : Module R✝ X✝
Y✝ : Type ?u.167554
inst✝¹⁷ : TopologicalSpace Y✝
inst✝¹⁶ : AddCommMonoid Y✝
inst✝¹⁵ : Module R✝ Y✝
Z : Type ?u.167587
inst✝¹⁴ : TopologicalSpace Z
inst✝¹³ : AddCommMonoid Z
inst✝¹² : Module R✝ Z
ι : Type ?u.167620
inst✝¹¹ : Fintype ι
E : ι → Type ?u.167628
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✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : TopologicalSemiring Y
f : X → Y
hf : IsContinuousLinearMap R f
y' : Y
⊢ ∀ (x : X), y' * f x = (ContinuousLinearMap.comp (ContinuousLinearMap.mul_left y') (mk' R f hf)) x
Tactic:
simp[ContinuousLinearMap.mul_left]
State after:
no goals