Theorem: SciLean.IsContinuousLinearMap.starRingEnd.arg_a.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝¹ : Type ?u.262135
inst✝⁴¹ : Semiring R✝¹
X✝² : Type ?u.262141
inst✝⁴⁰ : TopologicalSpace X✝²
inst✝³⁹ : AddCommMonoid X✝²
inst✝³⁸ : Module R✝¹ X✝²
Y✝² : Type ?u.262175
inst✝³⁷ : TopologicalSpace Y✝²
inst✝³⁶ : AddCommMonoid Y✝²
inst✝³⁵ : Module R✝¹ Y✝²
R✝ : Type ?u.262207
inst✝³⁴ : Semiring R✝
X✝¹ : Type ?u.262213
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝ X✝¹
Y✝¹ : Type ?u.262247
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝ Y✝¹
Z✝ : Type ?u.262279
inst✝²⁷ : TopologicalSpace Z✝
inst✝²⁶ : AddCommMonoid Z✝
inst✝²⁵ : Module R✝ Z✝
ι✝ : Type ?u.262311
inst✝²⁴ : Fintype ι✝
E✝ : ι✝ → Type ?u.262319
inst✝²³ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²² : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²¹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.262369
inst✝²⁰ : Semiring R
X✝ : Type ?u.262375
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R X✝
Y✝ : Type ?u.262410
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R Y✝
Z : Type ?u.262443
inst✝¹³ : TopologicalSpace Z
inst✝¹² : AddCommMonoid Z
inst✝¹¹ : Module R Z
ι : Type ?u.262476
inst✝¹⁰ : Fintype ι
E : ι → Type ?u.262484
inst✝⁹ : (i : ι) → TopologicalSpace (E i)
inst✝⁸ : (i : ι) → AddCommMonoid (E i)
inst✝⁷ : (i : ι) → Module R (E i)
K : Type u_1
inst✝⁶ : RCLike K
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module K X
Y : Type ?u.262741
inst✝² : NormedAddCommGroup Y
inst✝¹ : InnerProductSpace K Y
inst✝ : CompleteSpace Y
f : X → K
x✝ : IsContinuousLinearMap K f
⊢ IsContinuousLinearMap K fun x => (starRingEnd K) (f x)
Tactic:
sorry_proof
State after:
no goals