-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basis
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
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)),
        if x_1.1 = x_1.2 then
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.1 : R)
            (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
              ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.2 : R)
              ((Q : (a : M) → N) ((bm : (a : ι) → M) x_1.1 : M) : N))
        else
          if x_1.1 < x_1.2 then
            HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.1 : R)
              (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
                ((((bm.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1.2 : R)
                (polar.{u_3, u_4} (M := M) ((⇑Q : (a : M) → N) : (a : M) → N) ((bm : (a : ι) → M) x_1.1 : M)
                  ((bm : (a : ι) → M) x_1.2 : M)))
          else 0) =
    (Q : (a : M) → N)
      (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
        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))
⊢ Eq.{u_4 + 1} (α := N)
    (((Q.toBilin bm : (a : M) → M →ₗ[R] N)
            (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
              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)) :
          (a : M) → N)
        (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
          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)) :
      N)
    ((Q : (a : M) → N)
        (∑ a ∈ Finsupp.support.{u_1, u_2} (M := R) ((bm.repr : (a : M) → ι →₀ R) x),
          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)) :
      N)

Tactic:
simp_rw [LinearMap.map_sum₂, map_sum, LinearMap.map_smul₂, map_smul, toBilin_apply,
    smul_ite, smul_zero, ← Finset.sum_product', ← Finset.diag_union_offDiag,
    Finset.sum_union (Finset.disjoint_diag_offDiag _), Finset.sum_diag, if_true]

Premises used: if_true, Finset.sum_diag, Finset.diag_union_offDiag, smul_zero, QuadraticMap.toBilin_apply, Finset.sum_union, map_sum, Finset.sum_product', smul_ite, LinearMap.map_smul₂, LinearMap.map_sum₂, Finset.disjoint_diag_offDiag, map_smul