awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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 * (w₂ x_1 * ⟪v₁ x, 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]
-- 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
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
simp_rw₃ :
  ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ⟪v₁ x, v₂ x_1⟫_ℝ) =
    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 * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖ - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖) / 2)) =
  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
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
simp_rw₃ :
  ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ⟪v₁ x, v₂ x_1⟫_ℝ) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₄ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖ - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖) / 2)) =
    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 * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖) / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
  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
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
simp_rw₃ :
  ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ⟪v₁ x, v₂ x_1⟫_ℝ) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₄ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖ - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖) / 2)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₅ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖) / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    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 * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2 + ‖v₂ x_1‖ * ‖v₂ x_1‖ / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
  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
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
simp_rw₃ :
  ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ⟪v₁ x, v₂ x_1⟫_ℝ) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₄ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖ - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖) / 2)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₅ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖) / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₆ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        w₁ x * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2 + ‖v₂ x_1‖ * ‖v₂ x_1‖ / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    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 * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2 + ‖v₂ x_1‖ * ‖v₂ x_1‖ / 2)) -
        w₁ x * (w₂ x_1 * (‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2))) =
  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
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
simp_rw₃ :
  ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ⟪v₁ x, v₂ x_1⟫_ℝ) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₄ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖ - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖) / 2)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₅ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        w₁ x * (w₂ x_1 * ((‖v₁ x‖ * ‖v₁ x‖ + ‖v₂ x_1‖ * ‖v₂ x_1‖) / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₆ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        w₁ x * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2 + ‖v₂ x_1‖ * ‖v₂ x_1‖ / 2 - ‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₇ :
  ∑ x ∈ s₁,
      ∑ x_1 ∈ s₂,
        (w₁ x * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2 + ‖v₂ x_1‖ * ‖v₂ x_1‖ / 2)) -
          w₁ x * (w₂ x_1 * (‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2))) =
    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 * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2)) + w₁ x * (w₂ x_1 * (‖v₂ x_1‖ * ‖v₂ x_1‖ / 2)) -
        w₁ x * (w₂ x_1 * (‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2))) =
  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 : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ dist (HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x) (HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y) =
    √(HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2)
have rw : ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ =
  √(HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2)
Tactic: rw [dist_eq_norm, sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
rw :
  ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ =
    √(HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2)
⊢ dist (HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x) (HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y) =
    √(HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2)
have rw₁ : ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ =
  ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖
Tactic: rw [dist_eq_norm, sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ HPow.hPow (β := ℕ) ‖HPow.hPow (β := ℕ) (R / ‖x‖) 2 • x - HPow.hPow (β := ℕ) (R / ‖y‖) 2 • y‖ 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2
have simp : HPow.hPow (β := ℕ) R 4 * (HPow.hPow (β := ℕ) ‖y‖ 2 - 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖x‖ 2) =
  HPow.hPow (β := ℕ) R 4 * (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * ⟪x, y⟫_ℝ + HPow.hPow (β := ℕ) ‖y‖ 2)
Tactic: simp [field, sq, norm_sub_mul_self_real, norm_smul, real_inner_smul_left, inner_smul_right,
          Real.norm_of_nonneg (mul_self_nonneg _), -mul_eq_mul_left_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ √(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) =
    HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖) * dist x y
have rw : 0 ≤ ‖x - y‖
Tactic: rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
rw : 0 ≤ ‖x - y‖
⊢ √(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) =
    HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖) * dist x y
have rw₁ : 0 ≤ HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)
Tactic: rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
rw : 0 ≤ ‖x - y‖
rw₁ : 0 ≤ HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)
⊢ √(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) =
    HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖) * dist x y
have hx₁ : 0 ≤ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) R 2 / (‖x‖ * ‖y‖)) 2
Tactic: rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm]
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1
have hx' : ‖x‖ ≠ 0
Tactic: have hx' : ‖x‖ ≠ 0 := by simp [hx]
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1
have hr' : ‖r‖ ≠ 0
Tactic: have hr' : ‖r‖ ≠ 0 := by simp [hr]
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖⟪x, r • x⟫‖ / (‖x‖ * ‖r • x‖) = 1
have rw : ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
Tactic: rw [inner_smul_right, norm_mul, ← inner_self_re_eq_norm, inner_self_eq_norm_mul_norm, norm_smul]
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
have rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
Tactic: rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
have rw₁ : ‖r‖ * ‖x‖ * ‖x‖ / ‖x‖ / (‖r‖ * ‖x‖) = 1
Tactic: rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
rw₁ : ‖r‖ * ‖x‖ * ‖x‖ / ‖x‖ / (‖r‖ * ‖x‖) = 1
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
have rw₂ : ‖r‖ * ‖x‖ / (‖r‖ * ‖x‖) = 1
Tactic: rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
rw₁ : ‖r‖ * ‖x‖ * ‖x‖ / ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₂ : ‖r‖ * ‖x‖ / (‖r‖ * ‖x‖) = 1
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
have rw₃ : ‖r‖ * ‖x‖ / ‖r‖ / ‖x‖ = 1
Tactic: rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
rw₁ : ‖r‖ * ‖x‖ * ‖x‖ / ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₂ : ‖r‖ * ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₃ : ‖r‖ * ‖x‖ / ‖r‖ / ‖x‖ = 1
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
have rw₄ : ‖x‖ * ‖r‖ / ‖r‖ / ‖x‖ = 1
Tactic: rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
rw₁ : ‖r‖ * ‖x‖ * ‖x‖ / ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₂ : ‖r‖ * ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₃ : ‖r‖ * ‖x‖ / ‖r‖ / ‖x‖ = 1
rw₄ : ‖x‖ * ‖r‖ / ‖r‖ / ‖x‖ = 1
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
have rw₅ : ‖x‖ / ‖x‖ = 1
Tactic: rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']
-- 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
x : E
r : 𝕜
hx : x ≠ 0
hr : r ≠ 0
hx' : ‖x‖ ≠ 0
hr' : ‖r‖ ≠ 0
rw : ‖r‖ * ‖x‖ * ‖x‖ / (‖x‖ * (‖r‖ * ‖x‖)) = 1
rw₁ : ‖r‖ * ‖x‖ * ‖x‖ / ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₂ : ‖r‖ * ‖x‖ / (‖r‖ * ‖x‖) = 1
rw₃ : ‖r‖ * ‖x‖ / ‖r‖ / ‖x‖ = 1
rw₄ : ‖x‖ * ‖r‖ / ‖r‖ / ‖x‖ = 1
rw₅ : ‖x‖ / ‖x‖ = 1
⊢ ‖r‖ * (‖x‖ * ‖x‖) / (‖x‖ * (‖r‖ * ‖x‖)) = 1
have rw₆ : Eq (α := ℝ) 1 1
Tactic: rw [← mul_assoc, ← div_div, mul_div_cancel_right₀ _ hx', ← div_div, mul_comm,
    mul_div_cancel_right₀ _ hr', div_self hx']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1
have rw : r * (‖x‖ * ‖x‖) ≠ 0
Tactic: rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
    mul_assoc, abs_of_nonneg hr.le, div_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Basic (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = -1
have rw : r * (‖x‖ * ‖x‖) ≠ 0
Tactic: rw [real_inner_smul_self_right, norm_smul, Real.norm_eq_abs, ← mul_assoc ‖x‖, mul_comm _ |r|,
    mul_assoc, abs_of_neg hr, neg_mul, div_neg_eq_neg_div, div_self]
-- 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
x y : E
⊢ ∀ (a : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖), x = 0 ∨ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have refine : ∀ (h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖) (hx₀ : ¬x = 0), y = (⟪x, y⟫ / ⟪x, x⟫) • x
Tactic: refine fun h => or_iff_not_imp_left.2 fun hx₀ => ?_
-- 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
x y : E
h : ‖⟪x, y⟫‖ = ‖x‖ * ‖y‖
hx₀ : ¬x = 0
⊢ y = (⟪x, y⟫ / ⟪x, x⟫) • x
have this : HPow.hPow (β := ℕ) ‖x‖ 2 ≠ 0
Tactic: have : ‖x‖ ^ 2 ≠ 0 := pow_ne_zero _ (norm_ne_zero_iff.2 hx₀)