awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) ‖x - y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
have 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
Tactic: rw [sub_eq_add_neg, @norm_add_sq 𝕜 _ _ _ _ x (-y), norm_neg, inner_neg_right, map_neg, mul_neg,
    sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
have rw : HPow.hPow (β := ℕ) ‖x - y‖ 2 =
  ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
Tactic: rw [← sq (M := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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 =
    ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
have rw : HPow.hPow (β := ℕ) ‖x - y‖ 2 =
  HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
Tactic: rw [← sq (M := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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⟫ : ℝ) + ‖y‖ * ‖y‖
have rw : HPow.hPow (β := ℕ) ‖x - y‖ 2 =
  HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
    HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rw [← sq (M := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖
have repeat' : HPow.hPow (β := ℕ) ‖x - y‖ 2 =
  HPow.hPow (β := ℕ) ‖x‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
    HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: repeat' rw [← sq (M := ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
have h : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) + ‖y‖ * ‖y‖
Tactic: have h := @norm_sub_mul_self ℝ _ _ _ _ x y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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‖
have rw : ‖⟪x, y⟫‖ ≤ √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪y, y⟫)
Tactic: rw [norm_eq_sqrt_re_inner (𝕜 := 𝕜) x, norm_eq_sqrt_re_inner (𝕜 := 𝕜) y]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
have rw : ‖⟪x, y⟫‖ = 0
Tactic: rw [← norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
have refine : ‖⟪x, y⟫‖ ≤ 0
Tactic: refine le_antisymm ?_ (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ‖y‖ = 0
⊢ ⟪x, y⟫ = 0
have rw : ⟪y, x⟫ = 0
Tactic: rw [inner_eq_zero_symm, inner_eq_zero_of_left _ h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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
⊢ ⟪x, y⟫ = 0
have rw₁ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [inner_eq_zero_symm, inner_eq_zero_of_left _ h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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‖)
have 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⟫ : ℝ)
Tactic: simp only [← @inner_self_eq_norm_mul_norm 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ 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⟫ : ℝ)
have 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⟫ : ℝ)
Tactic: rw [← re.map_add, parallelogram_law, two_mul, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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 - y‖ 2 =
    2 * (HPow.hPow (β := ℕ) ‖x‖ 2 + HPow.hPow (β := ℕ) ‖y‖ 2)
have simp_rw : ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
Tactic: simp_rw [sq, parallelogram_law_with_norm_mul 𝕜 x y]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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 - y‖₊ 2 =
    2 * (HPow.hPow (β := ℕ) ‖x‖₊ 2 + HPow.hPow (β := ℕ) ‖y‖₊ 2)
have simp_rw : ‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊)
Tactic: simp_rw [sq, parallelogram_law_with_nnnorm_mul 𝕜 x y]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2
have rw : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
  (‖x‖ * ‖x‖ + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖ -
      ‖y‖ * ‖y‖) /
    2
Tactic: rw [@norm_add_mul_self 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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 - y‖ * ‖x - y‖) / 2
have rw : (re : (a : 𝕜) → ℝ) ⟪x, y⟫ =
  (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ -
      (‖x‖ * ‖x‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) + ‖y‖ * ‖y‖)) /
    2
Tactic: rw [@norm_sub_mul_self 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4
have 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
Tactic: rw [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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 - 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
have 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
Tactic: simp only [@norm_add_mul_self 𝕜, @norm_sub_mul_self 𝕜, inner_smul_right, I_mul_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
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‖) / 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
have 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
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0
have rw : Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) (0 : ℝ) ↔ ⟪x, y⟫_ℝ = 0
Tactic: rw [@norm_add_mul_self ℝ, add_right_cancel_iff, add_eq_left, mul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
have hx : 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: rw [← norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
have hy : 0 ≤ ‖x + y‖
Tactic: rw [← norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫ = 0
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
have rw : Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (0 : ℝ)
Tactic: rw [@norm_add_mul_self 𝕜, add_right_cancel_iff, add_eq_left, mul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫ = 0
⊢ Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (0 : ℝ)
have h₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) (0 : ℝ)
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0
have rw : Eq (α := ℝ) 2 0 ∨ Eq (α := ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) (0 : ℝ) ↔ ⟪x, y⟫_ℝ = 0
Tactic: rw [@norm_sub_mul_self ℝ, add_right_cancel_iff, sub_eq_add_neg, add_eq_left, neg_eq_zero,
    mul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
have hx : 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
Tactic: rw [← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : 0 ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
have hy : 0 ≤ ‖x - y‖
Tactic: rw [← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
    eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
| ‖x‖ = ‖y‖
have rw : ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖
have conv_rhs : ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
Tactic: conv_rhs => rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
have simp : ⟪x, x⟫_ℝ + ⟪y, x⟫_ℝ = ⟪y, x⟫_ℝ + ⟪y, y⟫_ℝ ↔ ⟪x, x⟫_ℝ = ⟪y, y⟫_ℝ
Tactic: simp only [← @inner_self_eq_norm_mul_norm ℝ, inner_add_left, inner_sub_right, real_inner_comm y x,
    sub_eq_zero, re_to_real]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
h : ⟪v, w⟫ = 0
⊢ ‖w - v‖ = ‖w + v‖
have rw : ‖w - v‖ * ‖w - v‖ = ‖w + v‖ * ‖w + v‖
Tactic: rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
⊢ |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1
have rw : |⟪x, y⟫_ℝ| / (‖x‖ * ‖y‖) ≤ 1
Tactic: rw [abs_div, abs_mul, abs_norm, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
⊢ ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
have rw : r * ⟪x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
Tactic: rw [real_inner_smul_left, ← real_inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
rw : r * ⟪x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
⊢ ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
have rw₁ : r * ⟪x, x⟫_ℝ = r * ⟪x, x⟫_ℝ
Tactic: rw [real_inner_smul_left, ← real_inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
⊢ ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)
have rw : r * ⟪x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
Tactic: rw [inner_smul_right, ← real_inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
rw : r * ⟪x, x⟫_ℝ = r * (‖x‖ * ‖x‖)
⊢ ⟪x, r • x⟫_ℝ = r * (‖x‖ * ‖x‖)
have rw₁ : r * ⟪x, x⟫_ℝ = r * ⟪x, x⟫_ℝ
Tactic: rw [inner_smul_right, ← real_inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : Eq (α := ℝ) (∑ i ∈ s₁, w₁ i) 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : Eq (α := ℝ) (∑ i ∈ s₂, w₂ i) 0
⊢ inner.{0, u_3} ℝ (E := F) (∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁) (∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
have simp_rw : ∑ i ∈ s₁, ⟪w₁ i • v₁ i, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
  HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
Tactic: simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
    real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
    add_div, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
    Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
    mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
    Finset.sum_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : Eq (α := ℝ) (∑ i ∈ s₁, w₁ i) 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : Eq (α := ℝ) (∑ i ∈ s₂, w₂ i) 0
simp_rw :
  ∑ i ∈ s₁, ⟪w₁ i • v₁ i, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
⊢ inner.{0, u_3} ℝ (E := F) (∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁) (∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
have simp_rw₁ : ∑ x ∈ s₁, ∑ i ∈ s₂, ⟪w₁ x • v₁ x, w₂ i • v₂ i⟫_ℝ =
  HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
Tactic: simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
    real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
    add_div, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
    Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
    mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
    Finset.sum_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : Eq (α := ℝ) (∑ i ∈ s₁, w₁ i) 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : Eq (α := ℝ) (∑ i ∈ s₂, w₂ i) 0
simp_rw :
  ∑ i ∈ s₁, ⟪w₁ i • v₁ i, ∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂⟫_ℝ =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₁ :
  ∑ x ∈ s₁, ∑ i ∈ s₂, ⟪w₁ x • v₁ x, w₂ i • v₂ i⟫_ℝ =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
⊢ inner.{0, u_3} ℝ (E := F) (∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁) (∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
have simp_rw₂ : ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * ⟪v₁ x, w₂ x_1 • v₂ x_1⟫_ℝ =
  HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
Tactic: simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
    real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
    add_div, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
    Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, zero_mul,
    mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
    Finset.sum_div, mul_div_assoc, mul_assoc]