awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖ : 𝕜) : 𝕜)
refine_1 : ‖g‖ ≤ 1
refine_2 : 1 ≤ ‖g‖
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
refine ⟨g, le_antisymm ?_ ?_, hval⟩
-- 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‖ : 𝕜) : 𝕜)
refine_1 : ‖x‖ * ‖coord‖ ≤ 1
⊢ ‖g‖ ≤ 1

Tactic:
simp only [hg.right, norm_smul, norm_algebraMap', norm_norm]

Premises used: norm_smul, norm_norm, And.right, norm_algebraMap'
-- 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‖ : 𝕜) : 𝕜)
⊢ 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
y : ↥(𝕜 ∙ x)
⊢ 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
h₁ : 0 ≤ ‖x‖
refine_1 : ‖x‖ * ‖x‖⁻¹ ≤ 1
refine_1₁ refine_1₂ : LE.le (α := ℝ) 1 1
⊢ ‖x‖ * ‖coord‖ ≤ 1

Tactic:
grw [coord.opNorm_le_bound (by positivity)
      (fun y ↦ (homothety_inverse _ (by positivity) _ hhomothety y).le), mul_inv_cancel₀ h]

Premises used: Norm.norm, ne_zero_of_norm_ne_zero, mul_inv_cancel₀, Eq.le, ContinuousLinearMap.opNorm_le_bound, ContinuousLinearEquiv.homothety_inverse, LinearEquiv.toSpanNonzeroSingleton
-- 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‖ : 𝕜) : 𝕜)
⊢ norm.{v} (E := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ≤ ‖g‖ * ‖x‖

Tactic:
have hle := g.le_opNorm x
-- 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‖ : 𝕜) : 𝕜)
hle : norm.{v} (E := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ≤ ‖g‖ * ‖x‖
⊢ ‖x‖ ≤ ‖g‖ * ‖x‖

Tactic:
simp only [hval, norm_algebraMap', norm_norm] at hle

Premises used: norm_norm, norm_algebraMap'
-- 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‖ : 𝕜) : 𝕜)
hle : ‖x‖ ≤ ‖g‖ * ‖x‖
⊢ 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‖
hval : Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)
hle : ‖x‖ ≤ ‖g‖ * ‖x‖
⊢ 1 ≤ ‖g‖

Tactic:
exact one_le_of_le_mul_right₀ (by positivity) hle

Premises used: one_le_of_le_mul_right₀
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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‖ : 𝕜) : 𝕜)
neg :
  ∀ (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‖ : 𝕜) : 𝕜)

Tactic:
by_cases hx : ‖x‖ = 0
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : ‖x‖ = 0
⊢ norm (E := StrongDual 𝕜 E) 0 ≤ 1

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
hx : ‖x‖ = 0
⊢ Eq.{v + 1} (α := 𝕜) ((0 : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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‖ : 𝕜) : 𝕜)

Tactic:
exact ⟨0, by simp, by simp [hx]⟩
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : ¬‖x‖ = 0
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‖ : 𝕜) : 𝕜)
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ ≤ 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
obtain ⟨g, hg⟩ := exists_dual_vector 𝕜 x hx

Premises used: exists_dual_vector
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : ¬‖x‖ = 0
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:
⟨g, hg.left.le, hg.right⟩

Premises used: Eq.le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type u
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
hx : ¬‖x‖ = 0
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:
exact ⟨g, hg.left.le, hg.right⟩
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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‖ : 𝕜) : 𝕜)
neg : ∀ (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‖ : 𝕜) : 𝕜)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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
pos :
  ∀ (y : E) (hy : ‖y‖ ≠ 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‖ : 𝕜) : 𝕜)

Tactic:
obtain ⟨y, hy⟩ := exists_norm_ne_zero E

Premises used: exists_norm_ne_zero
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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
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‖ : 𝕜) : 𝕜)
⊢ ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
obtain ⟨g, hg⟩ := exists_dual_vector 𝕜 y hy

Premises used: exists_dual_vector
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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
hg : ‖g‖ = 1 ∧ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) y : 𝕜) ((↑‖y‖ : 𝕜) : 𝕜)
⊢ Eq.{v + 1} (α := 𝕜) ((g : (a : E) → 𝕜) x : 𝕜) ((↑‖x‖ : 𝕜) : 𝕜)

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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
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:
exact ⟨g, hg.left, by simp [hx]⟩
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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‖ : 𝕜) : 𝕜)

Tactic:
exists_dual_vector 𝕜 x (norm_ne_zero_iff.mpr hx)

Premises used: Iff.mpr, exists_dual_vector, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.HahnBanach
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‖ : 𝕜) : 𝕜)

Tactic:
exact exists_dual_vector 𝕜 x (norm_ne_zero_iff.mpr hx)

Premises used: Iff.mpr, exists_dual_vector, norm_ne_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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
rw : ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖
⊢ ‖x‖ = ‖(1 - P) • x‖ + ‖(1 - (1 - P)) • x‖

Tactic:
rw [add_comm, sub_sub_cancel]

Premises used: add_comm, sub_sub_cancel
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖ = ‖P • x‖ + ‖(1 - P) • x‖

Tactic:
h.Lnorm x

Premises used: IsLprojection.Lnorm
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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‖ = ‖P • x‖ + ‖(1 - P) • x‖

Tactic:
exact h.Lnorm x

Premises used: IsLprojection.Lnorm
-- Module: Mathlib.Analysis.Normed.Module.MStructure
Goal:
X : Type u_1
inst : NormedAddCommGroup X
M : Type u_2
inst_1 : Ring M
inst_2 : Module M X
P : M
⊢ IsLprojection X P ↔ IsLprojection X (1 - P)

Tactic:
⟨Lcomplement, fun h => sub_sub_cancel 1 P ▸ h.Lcomplement⟩

Premises used: IsLprojection.Lcomplement, Eq.rec, sub_sub_cancel, Iff.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 - (R * P * R) • x‖ = 0
⊢ (P * R) • x = (R * P * R) • x

Tactic:
rw [← norm_sub_eq_zero_iff]

Premises used: norm_sub_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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)‖)
rw₆ 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‖)

Tactic:
rw [h₁.Lnorm, h₃.Lnorm, h₃.Lnorm ((1 - P) • R • x), sub_smul 1 P, one_smul, smul_sub,
              mul_smul]

Premises used: IsLprojection.Lnorm, HSub.hSub, sub_smul, one_smul, smul_sub, HSMul.hSMul, OfNat.ofNat, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 :
  ‖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‖)
rw₁ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖R • x - R • 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 • x - R • P • R • x‖ + ‖((1 - R) * R) • x - (1 - R) • P • R • x‖)
rw₂ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • (R • x - 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‖)
rw₃ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • R • x - (1 - R) • 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‖)
rw₄ rw₅ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • R • x - (1 - R) • 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‖)
⊢ ‖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‖)

Tactic:
rw [h₃.proj.eq, sub_smul 1 P, one_smul, smul_sub, mul_smul]

Premises used: sub_smul, one_smul, smul_sub, IsLprojection.proj, IsIdempotentElem.eq, OfNat.ofNat, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Normed.Module.MStructure
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 :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 * R - R * R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
rw₁ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 * R - R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
rw₂ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(R - R) • x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
rw₃ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ +
      (‖R • x - R • P • R • x‖ + ‖HSMul.hSMul.{u_2, u_1, u_1} (α := M) 0 x - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
rw₄ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖0 - (1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
rw₅ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖-((1 - R) • P • R • x)‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)
rw₆ rw₇ :
  ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • 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‖) =
    ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖)

Tactic:
rw [sub_mul, h₃.proj.eq, one_mul, sub_self, zero_smul, zero_sub, norm_neg]

Premises used: sub_self, sub_mul, zero_smul, norm_neg, IsLprojection.proj, IsIdempotentElem.eq, one_mul, zero_sub