-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
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'
⊢ 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))
have 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))
Tactic: apply sum_congr rfl