awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
repeat' :
  HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
repeat' rw [← sq (M := ℝ)]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
norm_add_sq _ _

Premises used: norm_add_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
exact norm_add_sq _ _

Premises used: norm_add_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) + ‖y‖ * ‖y‖

Tactic:
have h := @norm_add_mul_self ℝ _ _ _ _ x y
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) + ‖y‖ * ‖y‖
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  HPow.hPow (β := ℕ) ‖x + -y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
rw₁ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, -y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖-y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
rw₂ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, -y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
rw₃ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) (-⟪x, y⟫) : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
rw₄ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) (-(re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
rw₅ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + -HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
rw₆ rw₇ :
  HPow.hPow (β := ℕ) ‖x‖ 2 + -HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + -HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
rw [sub_eq_add_neg, @norm_add_sq 𝕜 _ _ _ _ x (-y), norm_neg, inner_neg_right, map_neg, mul_neg,
    sub_eq_add_neg]

Premises used: sub_eq_add_neg, inner_neg_right, map_neg, norm_add_sq, norm_neg, Neg.neg, mul_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
@norm_sub_sq ℝ _ _ _ _ _ _

Premises used: norm_sub_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
rw [← sq (M := ℝ)]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
repeat' :
  HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖

Tactic:
repeat' rw [← sq (M := ℝ)]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
norm_sub_sq _ _

Premises used: norm_sub_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
exact norm_sub_sq _ _

Premises used: norm_sub_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) + ‖y‖ * ‖y‖

Tactic:
have h := @norm_sub_mul_self ℝ _ _ _ _ x y
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
h : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) + ‖y‖ * ‖y‖
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖

Tactic:
simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw : ‖⟪x, y⟫‖ ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
⊢ ‖⟪x, y⟫‖ ≤ ‖x‖ * ‖y‖

Tactic:
rw [norm_eq_sqrt_re_inner (𝕜 := 𝕜) x, norm_eq_sqrt_re_inner (𝕜 := 𝕜) y]

Premises used: norm_eq_sqrt_re_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
this : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
⊢ ‖⟪x, y⟫‖ ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)

Tactic:
InnerProductSpace.Core.norm_inner_le_norm x y

Premises used: InnerProductSpace.Core.norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
this : PreInnerProductSpace.Core 𝕜 E := PreInnerProductSpace.toCore
⊢ ‖⟪x, y⟫‖ ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)

Tactic:
exact InnerProductSpace.Core.norm_inner_le_norm x y

Premises used: InnerProductSpace.Core.norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ‖⟪x, y⟫‖₊ ≤ ‖x‖₊ * ‖y‖₊

Tactic:
norm_inner_le_norm x y

Premises used: norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ ≤ ‖x‖ * ‖y‖

Tactic:
le_trans (re_le_norm ⟪x, y⟫) (norm_inner_le_norm x y)

Premises used: Inner.inner, RCLike.re_le_norm, norm_inner_le_norm, le_trans
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ |⟪x, y⟫_ℝ| ≤ ‖x‖ * ‖y‖

Tactic:
(Real.norm_eq_abs _).ge.trans (norm_inner_le_norm x y)

Premises used: Eq.ge, LE.le.trans, Real.norm_eq_abs, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ ≤ ‖x‖ * ‖y‖

Tactic:
le_trans (le_abs_self _) (abs_real_inner_le_norm _ _)

Premises used: le_abs_self, abs_real_inner_le_norm, le_trans
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
rw : ‖⟪x, y⟫‖ = 0
⊢ ⟪x, y⟫ = 0

Tactic:
rw [← norm_eq_zero]

Premises used: norm_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ 0 ≤ ‖⟪x, y⟫‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
refine : ‖⟪x, y⟫‖ ≤ 0
⊢ ‖⟪x, y⟫‖ = 0

Tactic:
refine le_antisymm ?_ (by positivity)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ‖x‖ * ‖y‖ ≤ 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖x‖ = 0
⊢ ‖⟪x, y⟫‖ ≤ 0

Tactic:
exact norm_inner_le_norm _ _ |>.trans <| by simp [h]

Premises used: LE.le.trans, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖y‖ = 0
rw : ⟪y, x⟫ = 0
rw₁ rw₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪x, y⟫ = 0

Tactic:
rw [inner_eq_zero_symm, inner_eq_zero_of_left _ h]

Premises used: inner_eq_zero_of_left, inner_eq_zero_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
simp :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) =
    2 * HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

Tactic:
simp only [← @inner_self_eq_norm_mul_norm 𝕜]

Premises used: inner_self_eq_norm_mul_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  (re : (a : 𝕜) → ℝ) (⟪x, x⟫ + ⟪y, y⟫ + (⟪x, x⟫ + ⟪y, y⟫)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x - y, x - y⟫ : ℝ) =
    2 * HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
rw [← re.map_add, parallelogram_law, two_mul, two_mul]

Premises used: two_mul, parallelogram_law, RCLike.re, AddMonoidHom.map_add
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (re : (a : 𝕜) → ℝ) (⟪x, x⟫ + ⟪y, y⟫ + (⟪x, x⟫ + ⟪y, y⟫)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ) +
      HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)

Tactic:
simp only [re.map_add]

Premises used: RCLike.re, AddMonoidHom.map_add
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
simp_rw : ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 + HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    2 * (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2)

Tactic:
simp_rw [sq, parallelogram_law_with_norm_mul 𝕜 x y]

Premises used: parallelogram_law_with_norm_mul, sq
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊)

Tactic:
Subtype.ext <| parallelogram_law_with_norm_mul 𝕜 x y

Premises used: parallelogram_law_with_norm_mul, NNReal, Subtype.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
simp_rw : ‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊)
⊢ HPow.hPow (β := ℕ) ‖x + y‖₊ 2 + HPow.hPow (β := ℕ) ‖x - y‖₊ 2 =
    2 * (HPow.hPow (β := ℕ) ‖x‖₊ 2 + HPow.hPow (β := ℕ) ‖y‖₊ 2)

Tactic:
simp_rw [sq, parallelogram_law_with_nnnorm_mul 𝕜 x y]

Premises used: sq, parallelogram_law_with_nnnorm_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖ -
        ‖y‖ * ‖y‖) /
      2
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Tactic:
rw [@norm_add_mul_self 𝕜]

Premises used: norm_add_mul_self
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖ -
        ‖y‖ * ‖y‖) /
      2

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ -
        (‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖)) /
      2
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

Tactic:
rw [@norm_sub_mul_self 𝕜]

Premises used: norm_sub_mul_self
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ -
        (‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖)) /
      2

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖ -
        (‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖)) /
      4
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4

Tactic:
rw [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜]

Premises used: norm_sub_mul_self, norm_add_mul_self
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖ -
        (‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖)) /
      4

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
simp :
  (im : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
          ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ -
        (‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
          ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖)) /
      4
⊢ (im : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ -
        ‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖) /
      4

Tactic:
simp only [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜, inner_smul_right, I_mul_re]

Premises used: norm_sub_mul_self, inner_smul_right, norm_add_mul_self, RCLike.I_mul_re
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (im : (a : 𝕜) → ℝ) ⟪x, y⟫ =
    (‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
          ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ -
        (‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) (-(im : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
          ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖)) /
      4

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
rw :
  (↑((‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4) : 𝕜) +
      HMul.hMul (α := 𝕜)
        (↑((‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ -
                ‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖) /
              4) :
          𝕜)
        I =
    (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + y‖ : 𝕜) 2 - HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - y‖ : 𝕜) 2 +
        (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2 -
            HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2) *
          I) /
      4
⊢ ⟪x, y⟫ =
    (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + y‖ : 𝕜) 2 - HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - y‖ : 𝕜) 2 +
        (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2 -
            HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2) *
          I) /
      4

Tactic:
rw [← re_add_im ⟪x, y⟫, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four,
    im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four]

Premises used: im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
push_cast :
  (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜)) / 4 +
      (HMul.hMul (α := 𝕜) (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
              (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
              (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)) /
          4 *
        I =
    (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + y‖ : 𝕜) 2 - HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - y‖ : 𝕜) 2 +
        (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2 -
            HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2) *
          I) /
      4
⊢ (↑((‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4) : 𝕜) +
      HMul.hMul (α := 𝕜)
        (↑((‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ -
                ‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ * ‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖) /
              4) :
          𝕜)
        I =
    (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + y‖ : 𝕜) 2 - HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - y‖ : 𝕜) 2 +
        (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2 -
            HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2) *
          I) /
      4

Tactic:
push_cast
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (HMul.hMul (α := 𝕜) (↑‖x + y‖ : 𝕜) (↑‖x + y‖ : 𝕜) - HMul.hMul (α := 𝕜) (↑‖x - y‖ : 𝕜) (↑‖x - y‖ : 𝕜)) / 4 +
      (HMul.hMul (α := 𝕜) (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
              (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)
              (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜)) /
          4 *
        I =
    (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + y‖ : 𝕜) 2 - HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - y‖ : 𝕜) 2 +
        (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x - HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2 -
            HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I y‖ : 𝕜) 2) *
          I) /
      4

Tactic:
simp only [sq, ← mul_div_right_comm, ← add_div]

Premises used: sq, mul_div_right_comm, add_div
-- Module: Mathlib.Analysis.InnerProductSpace.Basic
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x, y⟫_ℝ = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Tactic:
re_to_real.symm.trans <|
    re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two x y

Premises used: re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, RCLike.re_to_real, Eq.symm, Eq.trans