case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hinj : ker f = ⊥
hsurj : LinearMap.range f = ⊤
x✝ : E
⊢ ↑↑(ofBijective f hinj hsurj) x✝ = ↑f x✝
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hinj : ker f = ⊥
hsurj : LinearMap.range f = ⊤
⊢ ↑(ofBijective f hinj hsurj) = f
ext
no goals
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f✝ : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →L[𝕜] F
hinj : ker f = ⊥
hsurj : LinearMap.range f = ⊤
x✝ : E
⊢ ↑↑(ofBijective f hinj hsurj) x✝ = ↑f x✝
rfl