Theorem: SciLean.IsContinuousLinearMap.Inner.inner.arg_a1.IsContinuousLinearMap_rule (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R✝¹ : Type ?u.258319
inst✝⁴¹ : Semiring R✝¹
X✝² : Type ?u.258325
inst✝⁴⁰ : TopologicalSpace X✝²
inst✝³⁹ : AddCommMonoid X✝²
inst✝³⁸ : Module R✝¹ X✝²
Y✝² : Type ?u.258359
inst✝³⁷ : TopologicalSpace Y✝²
inst✝³⁶ : AddCommMonoid Y✝²
inst✝³⁵ : Module R✝¹ Y✝²
R✝ : Type ?u.258391
inst✝³⁴ : Semiring R✝
X✝¹ : Type ?u.258397
inst✝³³ : TopologicalSpace X✝¹
inst✝³² : AddCommMonoid X✝¹
inst✝³¹ : Module R✝ X✝¹
Y✝¹ : Type ?u.258431
inst✝³⁰ : TopologicalSpace Y✝¹
inst✝²⁹ : AddCommMonoid Y✝¹
inst✝²⁸ : Module R✝ Y✝¹
Z✝ : Type ?u.258463
inst✝²⁷ : TopologicalSpace Z✝
inst✝²⁶ : AddCommMonoid Z✝
inst✝²⁵ : Module R✝ Z✝
ι✝ : Type ?u.258495
inst✝²⁴ : Fintype ι✝
E✝ : ι✝ → Type ?u.258503
inst✝²³ : (i : ι✝) → TopologicalSpace (E✝ i)
inst✝²² : (i : ι✝) → AddCommMonoid (E✝ i)
inst✝²¹ : (i : ι✝) → Module R✝ (E✝ i)
R : Type ?u.258553
inst✝²⁰ : Semiring R
X✝ : Type ?u.258559
inst✝¹⁹ : TopologicalSpace X✝
inst✝¹⁸ : AddCommMonoid X✝
inst✝¹⁷ : Module R X✝
Y✝ : Type ?u.258594
inst✝¹⁶ : TopologicalSpace Y✝
inst✝¹⁵ : AddCommMonoid Y✝
inst✝¹⁴ : Module R Y✝
Z : Type ?u.258627
inst✝¹³ : TopologicalSpace Z
inst✝¹² : AddCommMonoid Z
inst✝¹¹ : Module R Z
ι : Type ?u.258660
inst✝¹⁰ : Fintype ι
E : ι → Type ?u.258668
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_3
inst✝² : NormedAddCommGroup Y
inst✝¹ : InnerProductSpace K Y
inst✝ : CompleteSpace Y
f : X → Y
x✝ : IsContinuousLinearMap K f
y : Y
⊢ IsContinuousLinearMap K fun x => ⟪y, f x⟫_K
Tactic:
sorry_proof
State after:
no goals