-- 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
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
simp_rw₉ :
  HSub.hSub (α := ℝ)
      (∑ 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))))
      (∑ x ∈ s₁, ∑ x_1 ∈ s₂, 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
simp_rw₁₀ :
  HAdd.hAdd (α := ℝ) (∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2)))
        (∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * (‖v₂ x_1‖ * ‖v₂ x_1‖ / 2))) -
      ∑ x ∈ s₁, ∑ x_1 ∈ s₂, 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
simp_rw₁₁ :
  HAdd.hAdd (α := ℝ) (∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x‖ * ‖v₁ x‖ / 2))
        (∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₂ i‖ * ‖v₂ i‖ / 2)) -
      ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 2) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₁₂ :
  ∑ x ∈ s₁, w₁ x * ((∑ i ∈ s₂, w₂ i) * (‖v₁ x‖ * ‖v₁ x‖ / 2)) +
        HMul.hMul (α := ℝ) (∑ i ∈ s₁, w₁ i) (∑ i ∈ s₂, w₂ i * (‖v₂ i‖ * ‖v₂ i‖ / 2)) -
      ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 2) =
    HDiv.hDiv (α := ℝ) (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) 2
simp_rw₁₃ :
  ∑ x ∈ s₁, w₁ x * ((∑ i ∈ s₂, w₂ i) * (‖v₁ x‖ * ‖v₁ x‖ / 2)) +
        HMul.hMul (α := ℝ) 0 (∑ i ∈ s₂, w₂ i * (‖v₂ i‖ * ‖v₂ i‖ / 2)) -
      ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 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₁, w₁ x * (0 * (‖v₁ x‖ * ‖v₁ x‖ / 2)) + HMul.hMul (α := ℝ) 0 (∑ i ∈ s₂, w₂ i * (‖v₂ i‖ * ‖v₂ i‖ / 2)) -
    ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 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]