-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : LinearOrder ι
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
x : M
⊢ HAdd.hAdd (α := N)
      (∑ x_1 ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
            ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
            ((Q : (a : M) → N) ((bm : (a : ι) → M) x_1 : M) : N)))
      (∑ x_1 ∈ Finset.offDiag (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x)) with x_1.1 < x_1.2,
        polar (⇑Q : (a : M) → N)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
            ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.1 : R) ((bm : (a : ι) → M) x_1.1 : M))
          (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
            ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.2 : R) ((bm : (a : ι) → M) x_1.2 : M))) =
    HAdd.hAdd (α := N)
      (∑ i ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
        (Q : (a : M) → N)
          (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
            ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((bm : (a : ι) → M) i : M)))
      (∑ ij ∈ Finset.sym2 (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x)) with ¬ij.IsDiag,
        polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
          (Sym2.map
            (fun (a : ι) ↦
              HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((bm : (a : ι) → M) a : M))
            ij))
have H : HAdd.hAdd (α := N)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          ((Q : (a : M) → N) ((bm : (a : ι) → M) x_1 : M) : N)))
    (∑ x_1 ∈ Finset.offDiag (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x)) with x_1.1 < x_1.2,
      polar (⇑Q : (a : M) → N)
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
          ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.1 : R) ((bm : (a : ι) → M) x_1.1 : M))
        (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
          ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.2 : R) ((bm : (a : ι) → M) x_1.2 : M))) =
  HAdd.hAdd (α := N)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          ((Q : (a : M) → N) ((bm : (a : ι) → M) x_1 : M) : N)))
    (∑ i ∈ Finset.offDiag (Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x)) with i.1 < i.2,
      polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
        (Sym2.map
          (fun (a : ι) ↦
            HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
              ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((bm : (a : ι) → M) a : M))
          s(i.1, i.2)))
Tactic: simp_rw [QuadraticMap.map_smul, mul_smul, Finset.sum_sym2_filter_not_isDiag]