-- Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Goal:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst : CommSemiring R
inst_1 : Fintype n
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : DecidableEq m
inst_5 : Fintype n'
inst_6 : Fintype m'
inst_7 : DecidableEq n'
inst_8 : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
l : (n' → R) →ₗ[R] n → R
r : (m' → R) →ₗ[R] m → R
i : n'
j : m'
a :
  ∀ (x : n),
    Membership.mem (γ := Finset n) univ x →
      Eq.{u_16 + 1} (α := R)
        (Finsupp.sum
          ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
            ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
          fun (j : m) (yj : R) ↦
          ((((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
                      ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
                    n →₀ R) :
                  (a : n) → R)
                x :
              R) •>
            yj •>
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) x) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
                R))
        (∑ x_1 : m,
          HMul.hMul (β := R)
            (HMul.hMul (α := R) (β := R)
              ((of : (a : n → n' → R) → Matrix n n' R)
                  (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) x i :
                R)
              ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) x 1) : (m → R) →ₗ[R] R) :
                    (a : m → R) → R)
                  (Pi.single (M := fun (a : m) ↦ R) x_1 1) :
                R))
            ((of : (a : m → m' → R) → Matrix m m' R)
                (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x_1 j :
              R))
⊢ Eq.{u_16 + 1} (α := R)
    (∑ i_1 : n,
      Finsupp.sum
        ((Basis.repr (Pi.basisFun R m) : (a : m → R) → m →₀ R)
          ((r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1)))
        fun (j : m) (yj : R) ↦
        ((((Basis.repr (Pi.basisFun R n) : (a : n → R) → n →₀ R)
                    ((l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) i 1)) :
                  n →₀ R) :
                (a : n) → R)
              i_1 :
            R) •>
          yj •>
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i_1) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
              R))
    (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((of : (a : n → n' → R) → Matrix n n' R)
                (fun (i : n) (j : n') ↦ (l : (a : n' → R) → n → R) (Pi.single (M := fun (a : n') ↦ R) j 1) i) y i :
              R)
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) y 1) : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                (Pi.single (M := fun (a : m) ↦ R) x 1) :
              R))
          ((of : (a : m → m' → R) → Matrix m m' R)
              (fun (i : m) (j : m') ↦ (r : (a : m' → R) → m → R) (Pi.single (M := fun (a : m') ↦ R) j 1) i) x j :
            R))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl