-- Mathlib/Analysis/Normed/Operator/Banach.lean
theorem exists_nonlinearRightInverse_of_surjective (f : E →SL[σ] F)
    (hsurj : LinearMap.range f = ⊤) :
    ∃ fsymm : NonlinearRightInverse f, 0 < fsymm.nnnorm

Proof state:
case h
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] 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 := ⟨C, ⋯⟩, bound' := ⋯, right_inv' := ⋯ }.nnnorm

Tactic:
exact hC

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : LinearMap.range f = ⊤
⊢ ∃ fsymm, 0 < fsymm.nnnorm

Tactic:
choose C hC fsymm h using
  exists_preimage_norm_le _ (LinearMap.range_eq_top.1 hsurj)

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] 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

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] 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

Tactic:
use {
    toFun := fsymm
    nnnorm := ⟨C, hC.lt.le⟩
    bound' := fun y => (h y).2
    right_inv' := fun y => (h y).1 }

Result:
case h
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] 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 := ⟨C, ⋯⟩, bound' := ⋯, right_inv' := ⋯ }.nnnorm