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 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
h : g i * ⟪v i, v i⟫ = ⟪v i, g i • v i⟫
convert_3 : ∀ b ∈ s, b ≠ i → ⟪v i, g b • v b⟫ = 0
⊢ ∑ i_1 ∈ s, ⟪v i, g i_1 • v i_1⟫ = g i * ⟪v i, v i⟫
have convert_4 : i ∉ s → ⟪v i, g i • v i⟫ = 0
Tactic: convert! Finset.sum_eq_single (M := 𝕜) i ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ g i * ⟪v i, v i⟫ = ⟪v i, g i • v i⟫
have h : g i * ⟪v i, v i⟫ = g i * ⟪v i, v i⟫
Tactic: rw [inner_smul_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
j : ι
_hj : j ∈ s
hji : j ≠ i
⊢ ⟪v i, g j • v j⟫ = 0
have convert_3 : g j * ⟪v i, v j⟫ = 0
Tactic: rw [inner_smul_right, ho hji.symm, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
j : ι
_hj : j ∈ s
hji : j ≠ i
convert_3 : g j * ⟪v i, v j⟫ = 0
⊢ ⟪v i, g j • v j⟫ = 0
have convert_3₁ : g j * 0 = 0
Tactic: rw [inner_smul_right, ho hji.symm, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
j : ι
_hj : j ∈ s
hji : j ≠ i
convert_3 : g j * ⟪v i, v j⟫ = 0
convert_3₁ : g j * 0 = 0
⊢ ⟪v i, g j • v j⟫ = 0
have convert_3₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [inner_smul_right, ho hji.symm, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun (i j : ι) ↦ ⟪v i, v j⟫ = 0
s : Finset ι
g : ι → 𝕜
hg : Eq.{u_2 + 1} (α := E) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
⊢ g i = 0
have h' : g i * ⟪v i, v i⟫ = ⟪v i, ∑ j ∈ s, g j • v j⟫
Tactic: have h' : g i * ⟪v i, v i⟫ = ⟪v i, ∑ j ∈ s, g j • v j⟫ := by
    rw [inner_sum]
    symm
    convert! Finset.sum_eq_single (M := 𝕜) i ?_ ?_
    · rw [inner_smul_right]
    · intro j _hj hji
      rw [inner_smul_right, ho hji.symm, mul_zero]
    · exact fun h => False.elim (h hi)
-- 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 : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
have rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
Tactic: rw [@norm_eq_sqrt_re_inner 𝕜, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
    sqrt_mul_self inner_self_nonneg]
-- 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 : E
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
have rw₁ : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ =
  √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
Tactic: rw [@norm_eq_sqrt_re_inner 𝕜, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
    sqrt_mul_self inner_self_nonneg]
-- 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 : E
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = √((re : (a : 𝕜) → ℝ) ⟪x, x⟫) * √((re : (a : 𝕜) → ℝ) ⟪x, x⟫)
rw₁ :
  (re : (a : 𝕜) → ℝ) ⟪x, x⟫ =
    √(HMul.hMul (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ))
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
have rw₂ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
Tactic: rw [@norm_eq_sqrt_re_inner 𝕜, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
    sqrt_mul_self inner_self_nonneg]
-- 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 : E
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = HPow.hPow (β := ℕ) ‖x‖ 2
have rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
Tactic: rw [pow_two, 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 : E
rw : (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = ‖x‖ * ‖x‖
⊢ (re : (a : 𝕜) → ℝ) ⟪x, x⟫ = HPow.hPow (β := ℕ) ‖x‖ 2
have rw₁ : ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
Tactic: rw [pow_two, inner_self_eq_norm_mul_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (hypothesis)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
have h : (re : (a : ℝ) → ℝ) ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
Tactic: have h := @inner_self_eq_norm_mul_norm ℝ F _ _ _ x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
⊢ ⟪x, x⟫_ℝ = HPow.hPow (β := ℕ) ‖x‖ 2
have rw : ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
Tactic: rw [pow_two, 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
rw : ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
⊢ ⟪x, x⟫_ℝ = HPow.hPow (β := ℕ) ‖x‖ 2
have rw₁ : ‖x‖ * ‖x‖ = ‖x‖ * ‖x‖
Tactic: rw [pow_two, real_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
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
have rw : (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
    HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rw [sq (M := ℝ), ← @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
⊢ (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
have rw : (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
  HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
      (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)) +
    HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: rw [sq (M := ℝ), ← @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
⊢ (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)) +
      HPow.hPow (β := ℕ) ‖y‖ 2
have rw : (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
  HAdd.hAdd (β := ℝ)
    (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
      (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
    ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
Tactic: rw [sq (M := ℝ), ← @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
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) +
      HPow.hPow (β := ℕ) ‖y‖ 2
have repeat' : (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
  HAdd.hAdd (β := ℝ)
    (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
      (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
    ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
Tactic: repeat' rw [sq (M := ℝ), ← @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
⊢ (re : (a : 𝕜) → ℝ) ⟪x + y, x + y⟫ =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have rw : (re : (a : 𝕜) → ℝ) (⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫) =
  HAdd.hAdd (β := ℝ)
    (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
    ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
Tactic: rw [inner_add_add_self, 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
⊢ (re : (a : 𝕜) → ℝ) (⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫) =
    HAdd.hAdd (β := ℝ)
      (HAdd.hAdd (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫ : ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)))
      ((re : (a : 𝕜) → ℝ) ⟪y, y⟫ : ℝ)
have simp : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
Tactic: simp only [add_assoc, add_left_inj, add_right_inj, map_add]
-- 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
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
have rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_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
rw : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, y⟫ : 𝕜) : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
⊢ Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪y, x⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
have rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, y⟫ : ℝ)
Tactic: rw [← inner_conj_symm, conj_re]
-- 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
⊢ HPow.hPow (β := ℕ) ‖x + y‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖y‖ 2
have h : HPow.hPow (β := ℕ) ‖x + y‖ 2 =
  HPow.hPow (β := ℕ) ‖x‖ 2 + HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) ⟪x, y⟫_ℝ : ℝ) +
    HPow.hPow (β := ℕ) ‖y‖ 2
Tactic: have h := @norm_add_sq ℝ _ _ _ _ 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‖ = ‖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_add_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
⊢ 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 + -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
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⟫ : ℝ) +
      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
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
⊢ 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
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
⊢ 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
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
⊢ 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
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
⊢ 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]