simp
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✝
no goals