-- Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean
theorem opNorm_extend_le :
    ‖f.extend e h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing‖ ≤ N * ‖f‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
⊢ ‖f.extend e h_dense ⋯‖ ≤ ↑N * ‖f‖

Tactic:
refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ ?_) fun x ↦ ?_)

Result:
case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
⊢ 0 ≤ ↑N * ‖f‖

case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
⊢ Continuous fun x => ‖(f.extend e h_dense ⋯) x‖

case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
⊢ Continuous fun x => ↑N * ‖f‖ * ‖x‖

case refine_4
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
x : E
⊢ ‖(f.extend e h_dense ⋯) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖

Proof state:
case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
⊢ Continuous fun x => ↑N * ‖f‖ * ‖x‖

Tactic:
exact continuous_const.mul continuous_norm

Result:
no goals

Proof state:
case refine_4
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
x : E
⊢ ‖f x‖ ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
calc
  ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
  _ ≤ ‖f‖ * (N * ‖e x‖) := mul_le_mul_of_nonneg_left (h_e x) (norm_nonneg _)
  _ ≤ N * ‖f‖ * ‖e x‖ := by rw [mul_comm ↑N ‖f‖, mul_assoc]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
Fₗ : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup Fₗ
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜₂ F
inst✝² : NormedSpace 𝕜 Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
f : E →SL[σ₁₂] F
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
⊢ 0 ≤ ↑N * ‖f‖

Tactic:
cases le_total 0 N with
| inl hN => exact mul_nonneg hN (norm_nonneg _)
| inr hN =>
  have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
    (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
  obtain rfl : f = 0 := Subsingleton.elim ..
  simp

Result:
no goals