-- 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:
𝕜 : 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)) = ↑(re (f x)) - I * ↑(re (f (I • x)))

Tactic:
rfl

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‖
h : ∀ (x : ↥p), g.extendTo𝕜 ↑x = f x
⊢ ‖reCLM‖ * ‖f‖ = ‖f‖

Tactic:
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 𝕜
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Tactic:
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E

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
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Proof state:
case him
𝕜 : 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)))
⊢ im (↑(re (f x)) - I * ↑(re (f (I • x)))) = im (f x)

Tactic:
simp only [Algebra.id.smul_eq_mul, I_re, ofReal_im, AddMonoidHom.map_add, zero_sub, I_im',
  zero_mul, ofReal_re, mul_neg, mul_im, zero_add, ofReal_neg, mul_re,
  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)))
⊢ ↑(re (f x)) - I * ↑(re (f (I • x))) = f x

Tactic:
apply ext

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

case him
𝕜 : 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)))
⊢ im (↑(re (f x)) - I * ↑(re (f (I • x)))) = im (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
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Tactic:
let fr := reCLM.comp (f.restrictScalars ℝ)

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, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

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[𝕜] 𝕜
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Tactic:
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜

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 𝕜
⊢ ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖