awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
rw : 1 * ‖f‖ = ‖f‖
rw₁ rw₂ : ‖f‖ = ‖f‖
⊢ norm.{u_1} (E := StrongDual ℝ 𝕜) reCLM * ‖f‖ = ‖f‖

Tactic:
rw [reCLM_norm, one_mul]

Premises used: RCLike.reCLM_norm, one_mul
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
_ : norm.{u_1} (E := StrongDual ℝ 𝕜) reCLM * ‖f‖ = ‖f‖
⊢ norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) ≤ ‖f‖

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

Premises used: StrongDual.norm_extendRCLike, RCLike.reCLM, ContinuousLinearMap.opNorm_comp_le, StrongDual.extendRCLike
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
⊢ ‖f‖ ≤ norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E)

Tactic:
f.opNorm_le_bound (g.extendRCLike (𝕜 := 𝕜)).opNorm_nonneg
      fun x ↦ h x ▸ (g.extendRCLike (𝕜 := 𝕜) |>.le_opNorm x)

Premises used: ContinuousLinearMap.le_opNorm, Eq.rec, ContinuousLinearMap.opNorm_le_bound, StrongDual.extendRCLike, ContinuousLinearMap.opNorm_nonneg, Subtype.val
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
p : Subspace 𝕜 E
f : StrongDual.{u_1, u_2} 𝕜 ↥p
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
this_3 : IsScalarTower ℝ 𝕜 E
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fr : ↥p →L[ℝ] ℝ :=
  ContinuousLinearMap.comp.{0, 0, 0, u_2, u_1, 0} (σ₁₂ := RingHom.id ℝ) (M₂ := 𝕜) reCLM
    (ContinuousLinearMap.restrictScalars ℝ f)
g : StrongDual ℝ E
hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ)
hnormeq : ‖g‖ = ‖fr‖
h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
⊢ ‖f‖ ≤ norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E)

Tactic:
exact f.opNorm_le_bound (g.extendRCLike (𝕜 := 𝕜)).opNorm_nonneg
      fun x ↦ h x ▸ (g.extendRCLike (𝕜 := 𝕜) |>.le_opNorm x)

Premises used: ContinuousLinearMap.le_opNorm, Eq.rec, ContinuousLinearMap.opNorm_le_bound, StrongDual.extendRCLike, ContinuousLinearMap.opNorm_nonneg, Subtype.val
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (↥p) F
inst_6 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range :=
  finBasis 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
e : ContinuousLinearEquiv.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range)
  (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) :=
  b.equivFunL
fi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (↥p) 𝕜 :=
  fun (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦
    comp (σ₂₃ := RingHom.id 𝕜) (M₂ := ↥(↑f : ↥p →ₗ[𝕜] F).range)
      (((LinearMap.toContinuousLinearMap.{u_1, u_3, u_1} (𝕜 := 𝕜) (E := ↥(↑f : ↥p →ₗ[𝕜] F).range) (F' := 𝕜) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜 ≃ₗ[𝕜]
              ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜) :
          (a : ↥(↑f : ↥p →ₗ[𝕜] F).range →ₗ[𝕜] 𝕜) → ↥(↑f : ↥p →ₗ[𝕜] F).range →L[𝕜] 𝕜)
        (b.coord i))
      (f.codRestrict (↑f : ↥p →ₗ[𝕜] F).range ⋯)
choose :
  ∀ (gi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) → StrongDual 𝕜 E)
    (hgf :
      ∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) (x : ↥p),
        Eq.{u_1 + 1} (α := 𝕜) ((gi i : (a : E) → 𝕜) (↑x : E) : 𝕜) ((fi i : (a : ↥p) → 𝕜) x : 𝕜)),
    (∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)), ‖gi i‖ = ‖fi i‖) →
      ∃ (g : E →L[𝕜] F), f = g ∘SL p.subtypeL
⊢ ∃ (g : E →L[𝕜] F), f = g ∘SL p.subtypeL

Tactic:
choose gi hgf _ using fun i ↦ exists_extension_norm_eq p (fi i)

Premises used: exists_extension_norm_eq
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (↥p) F
inst_6 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range :=
  finBasis 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
e : ContinuousLinearEquiv.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range)
  (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) :=
  b.equivFunL
fi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (↥p) 𝕜 :=
  fun (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦
    comp (σ₂₃ := RingHom.id 𝕜) (M₂ := ↥(↑f : ↥p →ₗ[𝕜] F).range)
      (((LinearMap.toContinuousLinearMap.{u_1, u_3, u_1} (𝕜 := 𝕜) (E := ↥(↑f : ↥p →ₗ[𝕜] F).range) (F' := 𝕜) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜 ≃ₗ[𝕜]
              ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜) :
          (a : ↥(↑f : ↥p →ₗ[𝕜] F).range →ₗ[𝕜] 𝕜) → ↥(↑f : ↥p →ₗ[𝕜] F).range →L[𝕜] 𝕜)
        (b.coord i))
      (f.codRestrict (↑f : ↥p →ₗ[𝕜] F).range ⋯)
gi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) → StrongDual 𝕜 E
hgf :
  ∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) (x : ↥p),
    Eq.{u_1 + 1} (α := 𝕜) ((gi i : (a : E) → 𝕜) (↑x : E) : 𝕜) ((fi i : (a : ↥p) → 𝕜) x : 𝕜)
h_1 : ∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)), ‖gi i‖ = ‖fi i‖
h :
  f =
    ((↑f : ↥p →ₗ[𝕜] F).range.subtypeL ∘SL
        (↑e.symm : (Fin (finrank 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) →L[𝕜] ↥(↑f : ↥p →ₗ[𝕜] F).range) ∘SL
          pi (φ := fun (a : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦ 𝕜) gi) ∘SL
      p.subtypeL
⊢ ∃ (g : E →L[𝕜] F), f = g ∘SL p.subtypeL

Tactic:
use f.range.subtypeL.comp <| e.symm.toContinuousLinearMap.comp (.pi gi)

Premises used: ContinuousLinearMap.comp, Submodule.subtypeL, ContinuousLinearEquiv.symm, ContinuousLinearMap.pi, LinearMap.range, ContinuousLinearMap.toLinearMap, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (↥p) F
inst_6 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range :=
  finBasis 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
e : ContinuousLinearEquiv.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range)
  (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) :=
  b.equivFunL
fi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (↥p) 𝕜 :=
  fun (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦
    comp (σ₂₃ := RingHom.id 𝕜) (M₂ := ↥(↑f : ↥p →ₗ[𝕜] F).range)
      (((LinearMap.toContinuousLinearMap.{u_1, u_3, u_1} (𝕜 := 𝕜) (E := ↥(↑f : ↥p →ₗ[𝕜] F).range) (F' := 𝕜) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜 ≃ₗ[𝕜]
              ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜) :
          (a : ↥(↑f : ↥p →ₗ[𝕜] F).range →ₗ[𝕜] 𝕜) → ↥(↑f : ↥p →ₗ[𝕜] F).range →L[𝕜] 𝕜)
        (b.coord i))
      (f.codRestrict (↑f : ↥p →ₗ[𝕜] F).range ⋯)
gi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) → StrongDual 𝕜 E
hgf :
  ∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) (x : ↥p),
    Eq.{u_1 + 1} (α := 𝕜) ((gi i : (a : E) → 𝕜) (↑x : E) : 𝕜) ((fi i : (a : ↥p) → 𝕜) x : 𝕜)
h_1 : ∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)), ‖gi i‖ = ‖fi i‖
h :
  ∀ (x : ↥p),
    Eq.{u_3 + 1} (α := F) ((f : (a : ↥p) → F) x : F)
      ((((↑f : ↥p →ₗ[𝕜] F).range.subtypeL ∘SL
                (↑e.symm : (Fin (finrank 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) →L[𝕜] ↥(↑f : ↥p →ₗ[𝕜] F).range) ∘SL
                  pi (φ := fun (a : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦ 𝕜) gi) ∘SL
              p.subtypeL :
            (a : ↥p) → F)
          x :
        F)
⊢ f =
    ((↑f : ↥p →ₗ[𝕜] F).range.subtypeL ∘SL
        (↑e.symm : (Fin (finrank 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) →L[𝕜] ↥(↑f : ↥p →ₗ[𝕜] F).range) ∘SL
          pi (φ := fun (a : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦ 𝕜) gi) ∘SL
      p.subtypeL

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
E : Type u_2
F : Type u_3
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
p : Submodule 𝕜 E
f : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (↥p) F
inst_6 : FiniteDimensional.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
b : Basis.{0, u_1, u_3} (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range :=
  finBasis 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range
e : ContinuousLinearEquiv.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range)
  (Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) :=
  b.equivFunL
fi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) →
  ContinuousLinearMap.{u_1, u_1, u_2, u_1} (RingHom.id 𝕜) (↥p) 𝕜 :=
  fun (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦
    comp (σ₂₃ := RingHom.id 𝕜) (M₂ := ↥(↑f : ↥p →ₗ[𝕜] F).range)
      (((LinearMap.toContinuousLinearMap.{u_1, u_3, u_1} (𝕜 := 𝕜) (E := ↥(↑f : ↥p →ₗ[𝕜] F).range) (F' := 𝕜) :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜 ≃ₗ[𝕜]
              ContinuousLinearMap.{u_1, u_1, u_3, u_1} (RingHom.id 𝕜) (↥(↑f : ↥p →ₗ[𝕜] F).range) 𝕜) :
          (a : ↥(↑f : ↥p →ₗ[𝕜] F).range →ₗ[𝕜] 𝕜) → ↥(↑f : ↥p →ₗ[𝕜] F).range →L[𝕜] 𝕜)
        (b.coord i))
      (f.codRestrict (↑f : ↥p →ₗ[𝕜] F).range ⋯)
gi : (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) → StrongDual 𝕜 E
hgf :
  ∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) (x : ↥p),
    Eq.{u_1 + 1} (α := 𝕜) ((gi i : (a : E) → 𝕜) (↑x : E) : 𝕜) ((fi i : (a : ↥p) → 𝕜) x : 𝕜)
h : ∀ (i : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)), ‖gi i‖ = ‖fi i‖
x : ↥p
⊢ Eq.{u_3 + 1} (α := F) ((f : (a : ↥p) → F) x : F)
    ((((↑f : ↥p →ₗ[𝕜] F).range.subtypeL ∘SL
              (↑e.symm : (Fin (finrank 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range) → 𝕜) →L[𝕜] ↥(↑f : ↥p →ₗ[𝕜] F).range) ∘SL
                pi (φ := fun (a : Fin (finrank.{u_1, u_3} 𝕜 ↥(↑f : ↥p →ₗ[𝕜] F).range)) ↦ 𝕜) gi) ∘SL
            p.subtypeL :
          (a : ↥p) → F)
        x :
      F)

Tactic:
simp [fi, e, hgf]
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
F : Type u_3
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
p : Submodule 𝕜 F
inst_4 : FiniteDimensional.{u_1, u_3} 𝕜 ↥p
⊢ p.ClosedComplemented

Tactic:
let ⟨g, hg⟩ := (ContinuousLinearMap.id 𝕜 p).exist_extension_of_finiteDimensional_range
  ⟨g, DFunLike.congr_fun hg.symm⟩

Premises used: DFunLike.congr_fun, Membership.mem, Subtype, ContinuousLinearMap.id, Submodule.ClosedComplemented, Exists.intro, ContinuousLinearMap.exist_extension_of_finiteDimensional_range, _private.0.Submodule.ClosedComplemented.of_finiteDimensional.match_1, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
⊢ ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖

Tactic:
have hhomothety := LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x (ne_zero_of_norm_ne_zero h)
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
⊢ 0 < ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
coord : ContinuousLinearMap.{v, v, u, v} (RingHom.id 𝕜) (↥(𝕜 ∙ x)) 𝕜 :=
  (↑(ContinuousLinearEquiv.symm
        (ofHomothety.{v, v, v, u} (E := 𝕜) (F := ↥(𝕜 ∙ x)) (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯
          hhomothety)) :
    ↥(𝕜 ∙ x) →L[𝕜] 𝕜)
g : StrongDual 𝕜 E
hg :
  (∀ (x_1 : ↥(𝕜 ∙ x)),
      Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x_1 : E) : 𝕜)
        ((HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord : (a : ↥(𝕜 ∙ x)) → 𝕜) x_1 : 𝕜)) ∧
    ‖g‖ = ‖HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord‖
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
coord : ContinuousLinearMap.{v, v, u, v} (RingHom.id 𝕜) (↥(𝕜 ∙ x)) 𝕜 :=
  (↑(ContinuousLinearEquiv.symm
        (ofHomothety.{v, v, v, u} (E := 𝕜) (F := ↥(𝕜 ∙ x)) (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯
          hhomothety)) :
    ↥(𝕜 ∙ x) →L[𝕜] 𝕜)
g : StrongDual 𝕜 E
hg :
  (∀ (x_1 : ↥(𝕜 ∙ x)),
      Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x_1 : E) : 𝕜)
        ((HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord : (a : ↥(𝕜 ∙ x)) → 𝕜) x_1 : 𝕜)) ∧
    ‖g‖ = ‖HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord‖
rw rw₁ : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((g : (a : E) → 𝕜) x : 𝕜)
⊢ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜)
    ((g : (a : E) → 𝕜) (↑(Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x ⋯) : E) :
      𝕜)

Tactic:
rw [Submodule.coe_mk]

Premises used: Submodule.coe_mk
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
coord : ContinuousLinearMap.{v, v, u, v} (RingHom.id 𝕜) (↥(𝕜 ∙ x)) 𝕜 :=
  (↑(ContinuousLinearEquiv.symm
        (ofHomothety.{v, v, v, u} (E := 𝕜) (F := ↥(𝕜 ∙ x)) (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯
          hhomothety)) :
    ↥(𝕜 ∙ x) →L[𝕜] 𝕜)
g : StrongDual 𝕜 E
hg :
  (∀ (x_1 : ↥(𝕜 ∙ x)),
      Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x_1 : E) : 𝕜)
        ((HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord : (a : ↥(𝕜 ∙ x)) → 𝕜) x_1 : 𝕜)) ∧
    ‖g‖ = ‖HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord‖
⊢ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜)
    ((g : (a : E) → 𝕜) (↑(Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x ⋯) : E) :
      𝕜)

Tactic:
have hgx : g x = g (⟨x, by simp⟩ : span 𝕜 {x}) := by rw [Submodule.coe_mk]
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
coord : ContinuousLinearMap.{v, v, u, v} (RingHom.id 𝕜) (↥(𝕜 ∙ x)) 𝕜 :=
  (↑(ContinuousLinearEquiv.symm
        (ofHomothety.{v, v, v, u} (E := 𝕜) (F := ↥(𝕜 ∙ x)) (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯
          hhomothety)) :
    ↥(𝕜 ∙ x) →L[𝕜] 𝕜)
g : StrongDual 𝕜 E
hg :
  (∀ (x_1 : ↥(𝕜 ∙ x)),
      Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x_1 : E) : 𝕜)
        ((HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord : (a : ↥(𝕜 ∙ x)) → 𝕜) x_1 : 𝕜)) ∧
    ‖g‖ = ‖HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord‖
hgx :
  Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜)
    ((g : (a : E) → 𝕜) (↑(Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x ⋯) : E) :
      𝕜)
⊢ Eq.{v + 1} (α := 𝕜)
    ((coord : (a : ↥(𝕜 ∙ x)) → 𝕜)
        (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x ⋯) :
      𝕜)
    (1 : 𝕜)

Tactic:
have hcx : coord ⟨x, _⟩ = 1 := LinearEquiv.coord_self 𝕜 E x (ne_zero_of_norm_ne_zero h)
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
coord : ContinuousLinearMap.{v, v, u, v} (RingHom.id 𝕜) (↥(𝕜 ∙ x)) 𝕜 :=
  (↑(ContinuousLinearEquiv.symm
        (ofHomothety.{v, v, v, u} (E := 𝕜) (F := ↥(𝕜 ∙ x)) (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯
          hhomothety)) :
    ↥(𝕜 ∙ x) →L[𝕜] 𝕜)
g : StrongDual 𝕜 E
hg :
  (∀ (x_1 : ↥(𝕜 ∙ x)),
      Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x_1 : E) : 𝕜)
        ((HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord : (a : ↥(𝕜 ∙ x)) → 𝕜) x_1 : 𝕜)) ∧
    ‖g‖ = ‖HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord‖
hgx :
  Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜)
    ((g : (a : E) → 𝕜) (↑(Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x ⋯) : E) :
      𝕜)
hcx :
  Eq.{v + 1} (α := 𝕜)
    ((coord : (a : ↥(𝕜 ∙ x)) → 𝕜)
        (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x ⋯) :
      𝕜)
    (1 : 𝕜)
⊢ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
simp [-algebraMap_smul, hgx, ↓hg.left, hcx]

Premises used: algebraMap_smul, And.left
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
coord : ContinuousLinearMap.{v, v, u, v} (RingHom.id 𝕜) (↥(𝕜 ∙ x)) 𝕜 :=
  (↑(ContinuousLinearEquiv.symm
        (ofHomothety.{v, v, v, u} (E := 𝕜) (F := ↥(𝕜 ∙ x)) (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯
          hhomothety)) :
    ↥(𝕜 ∙ x) →L[𝕜] 𝕜)
g : StrongDual 𝕜 E
hg :
  (∀ (x_1 : ↥(𝕜 ∙ x)),
      Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x_1 : E) : 𝕜)
        ((HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord : (a : ↥(𝕜 ∙ x)) → 𝕜) x_1 : 𝕜)) ∧
    ‖g‖ = ‖HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord‖
⊢ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
have hval : g x = ‖x‖ := by
    have hgx : g x = g (⟨x, by simp⟩ : span 𝕜 {x}) := by rw [Submodule.coe_mk]
    have hcx : coord ⟨x, _⟩ = 1 := LinearEquiv.coord_self 𝕜 E x (ne_zero_of_norm_ne_zero h)
    simp [-algebraMap_smul, hgx, ↓hg.left, hcx]
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
hhomothety :
  ∀ (c : 𝕜),
    norm.{u} (E := ↥(𝕜 ∙ x))
        (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯ : LinearEquiv.{v, v, v, u} (RingHom.id 𝕜) 𝕜 ↥(𝕜 ∙ x)) :
              (a : 𝕜) → ↥(𝕜 ∙ x))
            c :
          ↥(𝕜 ∙ x)) =
      ‖x‖ * ‖c‖
coord : ContinuousLinearMap.{v, v, u, v} (RingHom.id 𝕜) (↥(𝕜 ∙ x)) 𝕜 :=
  (↑(ContinuousLinearEquiv.symm
        (ofHomothety.{v, v, v, u} (E := 𝕜) (F := ↥(𝕜 ∙ x)) (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x ⋯) ‖x‖ ⋯
          hhomothety)) :
    ↥(𝕜 ∙ x) →L[𝕜] 𝕜)
g : StrongDual 𝕜 E
hg :
  (∀ (x_1 : ↥(𝕜 ∙ x)),
      Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x_1 : E) : 𝕜)
        ((HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord : (a : ↥(𝕜 ∙ x)) → 𝕜) x_1 : 𝕜)) ∧
    ‖g‖ = ‖HSMul.hSMul (α := 𝕜) (↑‖x‖ : 𝕜) coord‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
⟨g, le_antisymm ?_ ?_, hval⟩

Premises used: le_antisymm, And.intro, Exists.intro