𝕜 : 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
hsurj : LinearMap.range f = ⊤
C : ℝ
hC : C > 0
fsymm : F → E
h : ∀ (y : F), ↑f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ ∃ fsymm, 0 < fsymm.nnnorm
𝕜 : 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
hsurj : LinearMap.range f = ⊤
⊢ ∃ fsymm, 0 < fsymm.nnnorm
choose C hC fsymm h using exists_preimage_norm_le _ (LinearMap.range_eq_top.mp hsurj)
𝕜 : 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
hsurj : LinearMap.range f = ⊤
C : ℝ
hC : C > 0
fsymm : F → E
h : ∀ (y : F), ↑f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ 0 <
    { toFun := fsymm, nnnorm := { val := C, property := (_ : 0 ≤ C) }, bound' := (_ : ∀ (y : F), ‖fsymm y‖ ≤ C * ‖y‖),
        right_inv' := (_ : ∀ (y : F), ↑f (fsymm y) = y) }.nnnorm
𝕜 : 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
hsurj : LinearMap.range f = ⊤
C : ℝ
hC : C > 0
fsymm : F → E
h : ∀ (y : F), ↑f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ ∃ fsymm, 0 < fsymm.nnnorm
use {
    toFun := fsymm
    nnnorm := ⟨C, hC.lt.le⟩
    bound' := fun y => (h y).2
    right_inv' := fun y => (h y).1 }
no goals
𝕜 : 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
hsurj : LinearMap.range f = ⊤
C : ℝ
hC : C > 0
fsymm : F → E
h : ∀ (y : F), ↑f (fsymm y) = y ∧ ‖fsymm y‖ ≤ C * ‖y‖
⊢ 0 <
    { toFun := fsymm, nnnorm := { val := C, property := (_ : 0 ≤ C) }, bound' := (_ : ∀ (y : F), ‖fsymm y‖ ≤ C * ‖y‖),
        right_inv' := (_ : ∀ (y : F), ↑f (fsymm y) = y) }.nnnorm
exact hC