-- Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean
theorem exists_extension_norm_eq (p : Subspace ℝ E) (f : p →L[ℝ] ℝ) :
    ∃ g : E →L[ℝ] ℝ, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
c : ℝ
hc : 0 < c
x : E
⊢ (fun x => ‖f‖ * ‖x‖) (c • x) = c * (fun x => ‖f‖ * ‖x‖) x

Tactic:
simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
x y : E
⊢ (fun x => ‖f‖ * ‖x‖) (x + y) ≤ (fun x => ‖f‖ * ‖x‖) x + (fun x => ‖f‖ * ‖x‖) y

Tactic:
rw [← left_distrib]

Result:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
x y : E
⊢ (fun x => ‖f‖ * ‖x‖) (x + y) ≤ ‖f‖ * (‖x‖ + ‖y‖)

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Tactic:
refine ⟨g', g_eq, ?_⟩

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ‖g'‖ = ‖f‖

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Tactic:
rcases exists_extension_of_le_sublinear ⟨p, f⟩ (fun x => ‖f‖ * ‖x‖)
    (fun c hc x => by simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm])
    (fun x y => by rw [← left_distrib]
      exact mul_le_mul_of_nonneg_left (norm_add_le x y) (@norm_nonneg _ _ f))
    fun x => le_trans (le_abs_self _) (f.le_opNorm _) with ⟨g, g_eq, g_le⟩

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥p), g ↑x = f x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
⊢ ‖g ↑x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖

Tactic:
apply g'.le_opNorm

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
⊢ ‖f x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖

Tactic:
dsimp at g_eq

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥p), g ↑x = f x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
⊢ ‖f x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ‖g'‖ = ‖f‖

Tactic:
apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ‖f‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
x y : E
⊢ (fun x => ‖f‖ * ‖x‖) (x + y) ≤ ‖f‖ * (‖x‖ + ‖y‖)

Tactic:
exact mul_le_mul_of_nonneg_left (norm_add_le x y) (@norm_nonneg _ _ f)

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Tactic:
set g' :=
  g.mkContinuous ‖f‖ fun x => abs_le.2 ⟨neg_le.1 <| g.map_neg x ▸ norm_neg x ▸ g_le (-x), g_le x⟩

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥p), g ↑x = f x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
⊢ ‖f x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖

Tactic:
rw [← g_eq]

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥p), g ↑x = f x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
⊢ ‖g ↑x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
⊢ ‖f‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖

Tactic:
refine f.opNorm_le_bound (norm_nonneg _) fun x => ?_

Result:
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : ↥p →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥{ domain := p, toFun := ↑f }.domain), g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := g.mkContinuous ‖f‖ ⋯
x : ↥p
⊢ ‖f x‖ ≤ ‖g.mkContinuous ‖f‖ ⋯‖ * ‖x‖