-- 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:
case refine_1.inr
𝕜 : 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ₗ
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
hN : N ≤ 0
this : Unique E
⊢ 0 ≤ ↑N * ‖0‖

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.inr
𝕜 : 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 σ₁₂
hN : N ≤ 0
⊢ 0 ≤ ↑N * ‖f‖

Tactic:
have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
  (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩

Result:
case refine_1.inr
𝕜 : 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 σ₁₂
hN : N ≤ 0
this : Unique E
⊢ 0 ≤ ↑N * ‖f‖

Proof state:
case refine_1.inr
𝕜 : 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 σ₁₂
hN : N ≤ 0
this : Unique E
⊢ 0 ≤ ↑N * ‖f‖

Tactic:
obtain rfl : f = 0 := Subsingleton.elim ..

Result:
case refine_1.inr
𝕜 : 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ₗ
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : CompleteSpace F
e : E →L[𝕜] Fₗ
h_dense : DenseRange ⇑e
N : ℝ≥0
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
inst✝ : RingHomIsometric σ₁₂
hN : N ≤ 0
this : Unique E
⊢ 0 ≤ ↑N * ‖0‖

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 σ₁₂
x : E
⊢ ‖f‖ * (↑N * ‖e x‖) ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
rw [mul_comm ↑N ‖f‖, mul_assoc]

Result:
no goals

Proof state:
case refine_1.inl
𝕜 : 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 σ₁₂
hN : 0 ≤ N
⊢ 0 ≤ ↑N * ‖f‖

Tactic:
exact mul_nonneg hN (norm_nonneg _)

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.extend e h_dense ⋯) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
rw [extend_eq]

Result:
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‖

Proof state:
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‖

Tactic:
exact (cont _).norm

Result:
no goals