[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
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
      -- Porting note: placeholder filled here
      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_op_norm _) with
  ⟨g, g_eq, g_le⟩
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
c : ℝ
hc : 0 < c
x : E
⊢ (fun x => ‖f‖ * ‖x‖) (c • x) = c * (fun x => ‖f‖ * ‖x‖) x
[PROOFSTEP]
simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
x y : E
⊢ (fun x => ‖f‖ * ‖x‖) (x + y) ≤ (fun x => ‖f‖ * ‖x‖) x + (fun x => ‖f‖ * ‖x‖) y
[PROOFSTEP]
rw [← left_distrib]
[GOAL]
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
x y : E
⊢ (fun x => ‖f‖ * ‖x‖) (x + y) ≤ ‖f‖ * (‖x‖ + ‖y‖)
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left (norm_add_le x y) (@norm_nonneg _ _ f)
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
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⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
refine' ⟨g', g_eq, _⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
⊢ ‖g'‖ = ‖f‖
[PROOFSTEP]
apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
⊢ ‖f‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖
[PROOFSTEP]
refine' f.op_norm_le_bound (norm_nonneg _) fun x => _
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ { domain := p, toFun := ↑f }.domain }), ↑g ↑x = ↑{ domain := p, toFun := ↑f } x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
x : { x // x ∈ p }
⊢ ‖↑f x‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖ * ‖x‖
[PROOFSTEP]
dsimp at g_eq 
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
x : { x // x ∈ p }
⊢ ‖↑f x‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖ * ‖x‖
[PROOFSTEP]
rw [← g_eq]
[GOAL]
case intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
p : Subspace ℝ E
f : { x // x ∈ p } →L[ℝ] ℝ
g : E →ₗ[ℝ] ℝ
g_eq : ∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x
g_le : ∀ (x : E), ↑g x ≤ ‖f‖ * ‖x‖
g' : E →L[ℝ] ℝ := LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)
x : { x // x ∈ p }
⊢ ‖↑g ↑x‖ ≤ ‖LinearMap.mkContinuous g ‖f‖ (_ : ∀ (x : E), |↑g x| ≤ ‖f‖ * ‖x‖)‖ * ‖x‖
[PROOFSTEP]
apply g'.le_op_norm
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
letI : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
letI : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower _ _ _
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
letI : NormedSpace ℝ F :=
  NormedSpace.restrictScalars _ 𝕜
    _
      -- Let `fr: p →L[ℝ] ℝ` be the real part of `f`.
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
let fr :=
  reClm.comp
    (f.restrictScalars ℝ)
      -- Use the real version to get a norm-preserving extension of `fr`, which
        -- we'll call `g : F →L[ℝ] ℝ`.
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
rcases Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr with
  ⟨g, ⟨hextends, hnormeq⟩⟩
    -- Now `g` can be extended to the `F →L[𝕜] 𝕜` we need.
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ ∃ g, (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
[PROOFSTEP]
refine'
  ⟨g.extendTo𝕜, _⟩
    -- It is an extension of `f`.
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ (∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x) ∧ ‖ContinuousLinearMap.extendTo𝕜 g‖ = ‖f‖
[PROOFSTEP]
have h : ∀ x : p, g.extendTo𝕜 x = f x := by
  intro x
  rw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul, hextends, hextends]
  have : (fr x : 𝕜) - I * ↑(fr (I • x)) = (re (f x) : 𝕜) - (I : 𝕜) * re (f ((I : 𝕜) • x)) := by rfl
  rw [this]
  apply ext
  ·
    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]
  ·
    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]
      -- And we derive the equality of the norms by bounding on both sides.
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
⊢ ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
⊢ ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
[PROOFSTEP]
rw [ContinuousLinearMap.extendTo𝕜_apply, ← Submodule.coe_smul, hextends, hextends]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
⊢ ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑f x
[PROOFSTEP]
have : (fr x : 𝕜) - I * ↑(fr (I • x)) = (re (f x) : 𝕜) - (I : 𝕜) * re (f ((I : 𝕜) • x)) := by rfl
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // x ∈ p }
⊢ ↑(↑fr x) - I * ↑(↑fr (I • x)) = ↑(↑re (↑f x)) - I * ↑(↑re (↑f (I • x)))
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // 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
[PROOFSTEP]
rw [this]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // 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
[PROOFSTEP]
apply ext
[GOAL]
case hre
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // 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)
[PROOFSTEP]
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]
[GOAL]
case him
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝² : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝¹ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this✝ : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
x : { x // 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)
[PROOFSTEP]
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]
  -- And we derive the equality of the norms by bounding on both sides.
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ (∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x) ∧ ‖ContinuousLinearMap.extendTo𝕜 g‖ = ‖f‖
[PROOFSTEP]
refine' ⟨h, le_antisymm _ _⟩
[GOAL]
case intro.intro.refine'_1
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ ‖ContinuousLinearMap.extendTo𝕜 g‖ ≤ ‖f‖
[PROOFSTEP]
calc
  ‖g.extendTo𝕜‖ = ‖g‖ := g.norm_extendTo𝕜
  _ = ‖fr‖ := hnormeq
  _ ≤ ‖reClm‖ * ‖f‖ := (ContinuousLinearMap.op_norm_comp_le _ _)
  _ = ‖f‖ := by rw [reClm_norm, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ ‖reClm‖ * ‖f‖ = ‖f‖
[PROOFSTEP]
rw [reClm_norm, one_mul]
[GOAL]
case intro.intro.refine'_2
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
F : Type u_2
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : Subspace 𝕜 F
f : { x // x ∈ p } →L[𝕜] 𝕜
this✝¹ : Module ℝ F := RestrictScalars.module ℝ 𝕜 F
this✝ : IsScalarTower ℝ 𝕜 F := RestrictScalars.isScalarTower ℝ 𝕜 F
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
fr : { x // x ∈ p } →L[ℝ] ℝ := ContinuousLinearMap.comp reClm (ContinuousLinearMap.restrictScalars ℝ f)
g : F →L[ℝ] ℝ
hextends : ∀ (x : { x // x ∈ Submodule.restrictScalars ℝ p }), ↑g ↑x = ↑fr x
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : { x // x ∈ p }), ↑(ContinuousLinearMap.extendTo𝕜 g) ↑x = ↑f x
⊢ ‖f‖ ≤ ‖ContinuousLinearMap.extendTo𝕜 g‖
[PROOFSTEP]
exact f.op_norm_le_bound g.extendTo𝕜.op_norm_nonneg fun x => h x ▸ g.extendTo𝕜.le_op_norm x
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ‖↑‖x‖ • coord 𝕜 x h‖ = 1
[PROOFSTEP]
rw [norm_smul (x := coord 𝕜 x h), IsROrC.norm_coe_norm, coord_norm, mul_inv_cancel (mt norm_eq_zero.mp h)]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
let p : Submodule 𝕜 E := 𝕜 ∙ x
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
let f := (‖x‖ : 𝕜) • coord 𝕜 x h
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
obtain ⟨g, hg⟩ := exists_extension_norm_eq p f
[GOAL]
case intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
refine' ⟨g, _, _⟩
[GOAL]
case intro.refine'_1
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ‖g‖ = 1
[PROOFSTEP]
rw [hg.2, coord_norm']
[GOAL]
case intro.refine'_2
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g x = ↑‖x‖
[PROOFSTEP]
calc
  g x = g (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [coe_mk]
  _ = ((‖x‖ : 𝕜) • coord 𝕜 x h) (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [← hg.1]
  _ = ‖x‖ := by simp
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g x = ↑g ↑{ val := x, property := (_ : x ∈ span 𝕜 {x}) }
[PROOFSTEP]
rw [coe_mk]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑g ↑{ val := x, property := (_ : x ∈ span 𝕜 {x}) } =
    ↑(↑‖x‖ • coord 𝕜 x h) { val := x, property := (_ : x ∈ span 𝕜 {x}) }
[PROOFSTEP]
rw [← hg.1]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
p : Submodule 𝕜 E := span 𝕜 {x}
f : { x_1 // x_1 ∈ span 𝕜 {x} } →L[𝕜] 𝕜 := ↑‖x‖ • coord 𝕜 x h
g : E →L[𝕜] 𝕜
hg : (∀ (x : { x // x ∈ p }), ↑g ↑x = ↑f x) ∧ ‖g‖ = ‖f‖
⊢ ↑(↑‖x‖ • coord 𝕜 x h) { val := x, property := (_ : x ∈ span 𝕜 {x}) } = ↑‖x‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
obtain ⟨y, hy⟩ := exists_ne (0 : E)
[GOAL]
case pos.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
obtain ⟨g, hg⟩ : ∃ g : E →L[𝕜] 𝕜, ‖g‖ = 1 ∧ g y = ‖y‖ := exists_dual_vector 𝕜 y hy
[GOAL]
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
refine' ⟨g, hg.left, _⟩
[GOAL]
case pos.intro.intro
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : x = 0
y : E
hy : y ≠ 0
g : E →L[𝕜] 𝕜
hg : ‖g‖ = 1 ∧ ↑g y = ↑‖y‖
⊢ ↑g x = ↑‖x‖
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
𝕜 : Type v
inst✝³ : IsROrC 𝕜
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ = 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
exact exists_dual_vector 𝕜 x hx
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
refine' ⟨0, by simp, _⟩
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ‖0‖ ≤ 1
[PROOFSTEP]
simp
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ↑0 x = ↑‖x‖
[PROOFSTEP]
symm
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ↑‖x‖ = ↑0 x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
rcases exists_dual_vector 𝕜 x hx with ⟨g, g_norm, g_eq⟩
[GOAL]
case neg.intro.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : ¬x = 0
g : E →L[𝕜] 𝕜
g_norm : ‖g‖ = 1
g_eq : ↑g x = ↑‖x‖
⊢ ∃ g, ‖g‖ ≤ 1 ∧ ↑g x = ↑‖x‖
[PROOFSTEP]
exact ⟨g, g_norm.le, g_eq⟩
