awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have refine_1 : ‖g‖ ≤ 1
Tactic: refine ⟨g, le_antisymm ?_ ?_, hval⟩
-- 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
refine_1 : ‖g‖ ≤ 1
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have refine_2 : 1 ≤ ‖g‖
Tactic: refine ⟨g, le_antisymm ?_ ?_, hval⟩
-- 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ ‖g‖ ≤ 1
have refine_1 : ‖x‖ * ‖coord‖ ≤ 1
Tactic: simp only [hg.right, norm_smul, norm_algebraMap', norm_norm]
-- 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ ‖x‖ * ‖coord‖ ≤ 1
have h₁ : 0 ≤ ‖x‖
Tactic: grw [coord.opNorm_le_bound (by positivity)
      (fun y ↦ (homothety_inverse _ (by positivity) _ hhomothety y).le), mul_inv_cancel₀ 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
h₁ : 0 ≤ ‖x‖
⊢ ‖x‖ * ‖coord‖ ≤ 1
have refine_1 : ‖x‖ * ‖x‖⁻¹ ≤ 1
Tactic: grw [coord.opNorm_le_bound (by positivity)
      (fun y ↦ (homothety_inverse _ (by positivity) _ hhomothety y).le), mul_inv_cancel₀ 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
h₁ : 0 ≤ ‖x‖
refine_1 : ‖x‖ * ‖x‖⁻¹ ≤ 1
⊢ ‖x‖ * ‖coord‖ ≤ 1
have refine_1₁ : LE.le (α := ℝ) 1 1
Tactic: grw [coord.opNorm_le_bound (by positivity)
      (fun y ↦ (homothety_inverse _ (by positivity) _ hhomothety y).le), mul_inv_cancel₀ 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ 1 ≤ ‖g‖
have hle : norm.{v} (E := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ≤ ‖g‖ * ‖x‖
Tactic: have hle := g.le_opNorm 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
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‖ : 𝕜) : 𝕜)
hle : norm.{v} (E := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ≤ ‖g‖ * ‖x‖
⊢ 1 ≤ ‖g‖
have hle₁ : ‖x‖ ≤ ‖g‖ * ‖x‖
Tactic: simp only [hval, norm_algebraMap', norm_norm] at hle
Cleared hypotheses: hle
-- 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
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have pos : ∀ (hx : ‖x‖ = 0), ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
Tactic: by_cases hx : ‖x‖ = 0
-- 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
pos : ∀ (hx : ‖x‖ = 0), ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have neg : ∀ (hx : ¬‖x‖ = 0), ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
Tactic: by_cases hx : ‖x‖ = 0
-- 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
hx : ¬‖x‖ = 0
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have neg : ∀ (g : StrongDual 𝕜 E) (hg : ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)),
  ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
Tactic: obtain ⟨g, hg⟩ := exists_dual_vector 𝕜 x hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
x : E
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have pos : ∀ (hx : x = 0), ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
x : E
pos : ∀ (hx : x = 0), ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have neg : ∀ (hx : ¬x = 0), ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
x : E
hx : x = 0
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have pos : ∀ (y : E) (hy : ‖y‖ ≠ 0),
  ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
Tactic: obtain ⟨y, hy⟩ := exists_norm_ne_zero E
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.HahnBanach (goal)
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
x : E
hx : x = 0
y : E
hy : ‖y‖ ≠ 0
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
have pos : ∀ (g : StrongDual 𝕜 E) (hg : ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) y : 𝕜) ((↑‖y‖ : 𝕜) : 𝕜)),
  ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
Tactic: obtain ⟨g, hg⟩ := exists_dual_vector 𝕜 y hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
P : M
h : IsLprojection X P
x : X
⊢ ‖x‖ = ‖(1 - P) • x‖ + ‖(1 - (1 - P)) • x‖
have rw : ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖
Tactic: rw [add_comm, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ (P * R) • x = (R * P * R) • x
have rw : ‖(P * R) • x - (R * P * R) • x‖ = 0
Tactic: rw [← norm_sub_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
have rw : ‖P • R • x‖ + ‖(1 - P) • R • x‖ =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
Tactic: rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
rw :
  ‖P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
have rw₁ : ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + ‖(1 - P) • R • x‖ =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
Tactic: rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
rw :
  ‖P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₁ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
have rw₂ : ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (1 - P) • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
Tactic: rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
rw :
  ‖P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₁ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₂ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (1 - P) • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
have rw₃ : ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
    (‖R • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖ +
      ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖) =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
    (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖)
Tactic: rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
rw :
  ‖P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₁ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₂ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (1 - P) • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₃ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖R • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖ +
        ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖)
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
have rw₄ : ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (R • x - P • R • x)‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖)
Tactic: rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
rw :
  ‖P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₁ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₂ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (1 - P) • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₃ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖R • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖ +
        ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖)
rw₄ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (R • x - P • R • x)‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖)
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
have rw₅ : ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • R • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖)
Tactic: rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
rw :
  ‖P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₁ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + ‖(1 - P) • R • x‖ =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₂ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (1 - P) • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
rw₃ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖R • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖ +
        ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (HSMul.hSMul.{u_2, u_1, u_1} (α := M) 1 (R • x) - P • R • x)‖)
rw₄ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • (R • x - P • R • x)‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖)
rw₅ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • R • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖)
⊢ ‖R • x‖ = ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖)
have rw₆ : ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • R • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖) =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • R • x - R • P • R • x‖ + ‖(1 - R) • (R • x - P • R • x)‖)
Tactic: rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MStructure (goal)
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
inst_3 : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖(R * R) • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)
have rw : ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • (1 - P) • R • x‖) =
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)
Tactic: rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]