-- 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'
i' : n
a :
  ∀ (x : m),
    Membership.mem (γ := Finset m) univ x →
      ((((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' :
            R) •>
          ((((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)) :
                    m →₀ R) :
                  (a : m) → R)
                x :
              R) •>
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i') : (m → R) →ₗ[R] R) :
                  (a : m → R) → R)
                ((Pi.basisFun R m : (a : m) → m → R) x : m → R) :
              R) =
        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) i' i :
              R)
            ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i' 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)
⊢ Eq.{u_16 + 1} (α := R)
    (∑ i_1 : m,
      ((((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' :
          R) •>
        ((((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)) :
                  m →₀ R) :
                (a : m) → R)
              i_1 :
            R) •>
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) ((Pi.basisFun R n : (a : n) → n → R) i') : (m → R) →ₗ[R] R) :
                (a : m → R) → R)
              ((Pi.basisFun R m : (a : m) → m → R) i_1 : m → R) :
            R))
    (∑ 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) i' i :
            R)
          ((((B : (a : n → R) → (m → R) →ₗ[R] R) (Pi.single (M := fun (a : n) ↦ R) i' 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