awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (hypothesis)
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 : Module ℝ E := Module.restrictScalars ℝ 𝕜 E
⊢ ∃ (g : StrongDual 𝕜 E),
    (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖
have this₁ : IsScalarTower ℝ 𝕜 E
Tactic: haveI : IsScalarTower ℝ 𝕜 E := .restrictScalars _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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),
    (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖
have obtain : ∀ (g : StrongDual ℝ E) (hextends : ∀ (x : ↥p), Eq (α := ℝ) ((g : (a : E) → ℝ) (↑x : E) : ℝ) ((fr : (a : ↥p) → ℝ) x : ℝ))
  (hnormeq : ‖g‖ = ‖fr‖),
  ∃ (g : StrongDual 𝕜 E),
    (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖
Tactic: obtain ⟨g, ⟨(hextends : ∀ x : p, g x = fr x), hnormeq⟩⟩ :=
    Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖
⊢ ∃ (g : StrongDual 𝕜 E),
    (∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧ ‖g‖ = ‖f‖
have refine : (∀ (x : ↥p),
    Eq.{u_1 + 1} (α := 𝕜) (((g.extendRCLike : StrongDual 𝕜 E) : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧
  norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) = ‖f‖
Tactic: refine ⟨g.extendRCLike, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖
x : ↥p
⊢ Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
have rw : (↑((fr : (a : ↥p) → ℝ) x) : 𝕜) -
    HMul.hMul (α := 𝕜) I (↑((fr : (a : ↥p) → ℝ) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x)) : 𝕜) =
  (f : (a : ↥p) → 𝕜) x
Tactic: rw [g.extendRCLike_apply, ← Submodule.coe_smul,
      hextends, hextends]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (hypothesis)
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‖
⊢ (∀ (x : ↥p),
      Eq.{u_1 + 1} (α := 𝕜) (((g.extendRCLike : StrongDual 𝕜 E) : (a : E) → 𝕜) (↑x : E) : 𝕜)
        ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧
    norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) = ‖f‖
have h : ∀ (x : ↥p), Eq.{u_1 + 1} (α := 𝕜) ((g.extendRCLike : (a : E) → 𝕜) (↑x : E) : 𝕜) ((f : (a : ↥p) → 𝕜) x : 𝕜)
Tactic: have h (x : p) : g.extendRCLike x = f x := by
    rw [g.extendRCLike_apply, ← Submodule.coe_smul,
      hextends, hextends]
    simp [fr, RCLike.algebraMap_eq_ofReal, mul_comm I, RCLike.re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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 : 𝕜)
⊢ (∀ (x : ↥p),
      Eq.{u_1 + 1} (α := 𝕜) (((g.extendRCLike : StrongDual 𝕜 E) : (a : E) → 𝕜) (↑x : E) : 𝕜)
        ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧
    norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) = ‖f‖
have refine_1 : norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) ≤ ‖f‖
Tactic: refine ⟨h, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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 : 𝕜)
refine_1 : norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) ≤ ‖f‖
⊢ (∀ (x : ↥p),
      Eq.{u_1 + 1} (α := 𝕜) (((g.extendRCLike : StrongDual 𝕜 E) : (a : E) → 𝕜) (↑x : E) : 𝕜)
        ((f : (a : ↥p) → 𝕜) x : 𝕜)) ∧
    norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) = ‖f‖
have refine_2 : ‖f‖ ≤ norm (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E)
Tactic: refine ⟨h, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖
have rw : 1 * ‖f‖ = ‖f‖
Tactic: rw [reCLM_norm, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖
⊢ norm.{u_1} (E := StrongDual ℝ 𝕜) reCLM * ‖f‖ = ‖f‖
have rw₁ : ‖f‖ = ‖f‖
Tactic: rw [reCLM_norm, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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 (E := StrongDual 𝕜 E) (g.extendRCLike : StrongDual 𝕜 E) ≤ ‖f‖
have _ : norm.{u_1} (E := StrongDual ℝ 𝕜) reCLM * ‖f‖ = ‖f‖
Tactic: calc
      ‖g.extendRCLike‖ = ‖g‖ := g.norm_extendRCLike
      _ = ‖fr‖ := hnormeq
      _ ≤ ‖reCLM‖ * ‖f‖ := ContinuousLinearMap.opNorm_comp_le _ _
      _ = ‖f‖ := by rw [reCLM_norm, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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 ⋯)
⊢ ∃ (g : E →L[𝕜] F), f = g ∘SL p.subtypeL
have 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
Tactic: choose gi hgf _ using fun i ↦ exists_extension_norm_eq p (fi i)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖
⊢ ∃ (g : E →L[𝕜] F), f = g ∘SL p.subtypeL
have 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
Tactic: use f.range.subtypeL.comp <| e.symm.toContinuousLinearMap.comp (.pi gi)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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‖
⊢ 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
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (hypothesis)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
h : ‖x‖ ≠ 0
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have hhomothety : ∀ (c : 𝕜),
  norm.{u} (E := ↥(𝕜 ∙ x))
      (((LinearEquiv.toSpanNonzeroSingleton 𝕜 E x sorry : 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
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) :
      𝕜)
have rw : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((g : (a : E) → 𝕜) x : 𝕜)
Tactic: rw [Submodule.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (hypothesis)
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‖ : 𝕜) : 𝕜)
have 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 sorry) : E) : 𝕜)
Tactic: have hgx : g x = g (⟨x, by simp⟩ : span 𝕜 {x}) := by rw [Submodule.coe_mk]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (hypothesis)
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} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have hcx : Eq.{v + 1} (α := 𝕜)
  ((coord : (a : ↥(𝕜 ∙ x)) → 𝕜)
      (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ x) x_1) x sorry) :
    𝕜)
  (1 : 𝕜)
Tactic: have hcx : coord ⟨x, _⟩ = 1 := LinearEquiv.coord_self 𝕜 E x (ne_zero_of_norm_ne_zero h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (hypothesis)
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‖
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have hval : 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]