Theorem: SciLean.ContinuousLinearMap.eta_reduce (SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean)

State before:
R : Type u_3
inst✝⁶ : Semiring R
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module R X
Y : Type u_1
inst✝² : TopologicalSpace Y
inst✝¹ : AddCommMonoid Y
inst✝ : Module R Y
f : X →L[R] Y
⊢ mk' R ⇑f ⋯ = f
Tactic:
ext
State after:
case h
R : Type u_3
inst✝⁶ : Semiring R
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module R X
Y : Type u_1
inst✝² : TopologicalSpace Y
inst✝¹ : AddCommMonoid Y
inst✝ : Module R Y
f : X →L[R] Y
x✝ : X
⊢ (mk' R ⇑f ⋯) x✝ = f x✝

State before:
case h
R : Type u_3
inst✝⁶ : Semiring R
X : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : AddCommMonoid X
inst✝³ : Module R X
Y : Type u_1
inst✝² : TopologicalSpace Y
inst✝¹ : AddCommMonoid Y
inst✝ : Module R Y
f : X →L[R] Y
x✝ : X
⊢ (mk' R ⇑f ⋯) x✝ = f x✝
Tactic:
simp
State after:
no goals