-- 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:
case hre
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝² : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝¹ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
this : ↑(fr x) - I * ↑(fr (I • x)) = ↑(re (f x)) - I * ↑(re (f (I • x)))
⊢ re (↑(re (f x)) - I * ↑(re (f (I • x)))) = re (f x)

Tactic:
simp only [add_zero, Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub,
  I_im', zero_mul, ofReal_re, eq_self_iff_true, sub_zero, mul_neg, ofReal_neg,
  mul_re, mul_zero, sub_neg_eq_add, ContinuousLinearMap.map_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝² : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝¹ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
this : ↑(fr x) - I * ↑(fr (I • x)) = ↑(re (f x)) - I * ↑(re (f (I • x)))
⊢ ↑(fr x) - I * ↑(fr (I • x)) = f x

Tactic:
erw [this]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝² : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝¹ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
this : ↑(fr x) - I * ↑(fr (I • x)) = ↑(re (f x)) - I * ↑(re (f (I • x)))
⊢ ↑(re (f x)) - I * ↑(re (f (I • x))) = f x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
⊢ g.extendTo𝕜 ↑x = f x

Tactic:
erw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul, hextends, hextends]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
⊢ ↑(fr x) - I * ↑(fr (I • x)) = f x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ ∀ (x : ↥p), g.extendTo𝕜 ↑x = f x

Tactic:
intro x

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
x : ↥p
⊢ g.extendTo𝕜 ↑x = f x

Proof state:
case intro.intro.refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), g.extendTo𝕜 ↑x = f x
⊢ ‖g.extendTo𝕜‖ ≤ ‖f‖

Tactic:
calc
  ‖g.extendTo𝕜‖ = ‖g‖ := g.norm_extendTo𝕜
  _ = ‖fr‖ := hnormeq
  _ ≤ ‖reCLM‖ * ‖f‖ := ContinuousLinearMap.opNorm_comp_le _ _
  _ = ‖f‖ := by rw [reCLM_norm, one_mul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Tactic:
rcases Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr with ⟨g, ⟨hextends, hnormeq⟩⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : ↥p →L[𝕜] 𝕜
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)
g : E →L[ℝ] ℝ
hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖