-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.SesquilinearForm (goal)
Goal:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
inst_5 : Fintype n
inst_6 : Fintype m
inst_7 : DecidableEq m
inst_8 : DecidableEq n
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst_9 : AddCommMonoid M₁'
inst_10 : Module R M₁'
inst_11 : AddCommMonoid M₂'
inst_12 : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst_13 : Fintype n'
inst_14 : Fintype m'
inst_15 : DecidableEq n'
inst_16 : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
l : M₁' →ₗ[R] M₁
r : M₂' →ₗ[R] M₂
i : n'
j : m'
a :
  Eq.{u_1 + 1} (α := R)
    (∑ i_1 : n,
      Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
        fun (j : m) (yj : R) ↦
        ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                (a : n) → R)
              i_1 :
            R) •>
          yj •>
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i_1) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) j : M₂) :
              R))
    (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                  (a : n) → R)
                y :
              R)
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) y) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x : M₂) :
              R))
          ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              x :
            R))
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')))
      fun (i : n) (xi : R) ↦
      Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
        fun (j : m) (yj : R) ↦
        xi •>
          yj •>
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) j : M₂) :
              R))
    (∑ y : n,
      ∑ x : m,
        HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((((b₁.repr : (a : M₁) → n →₀ R) ((l : (a : M₁') → M₁) ((b₁' : (a : n') → M₁') i : M₁')) : n →₀ R) :
                  (a : n) → R)
                y :
              R)
            ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) y) : M₂ →ₗ[R] R) : (a : M₂) → R)
                ((b₂ : (a : m) → M₂) x : M₂) :
              R))
          ((((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')) : m →₀ R) :
                (a : m) → R)
              x :
            R))
have a₁ : ∀ (i : n),
  Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b₂.repr : (a : M₂) → m →₀ R) ((r : (a : M₂') → M₂) ((b₂' : (a : m') → M₂') j : M₂')))
      fun (j : m) (yj : R) ↦
      0 •>
        yj •>
          ((((B : (a : M₁) → M₂ →ₗ[R] R) ((b₁ : (a : n) → M₁) i) : M₂ →ₗ[R] R) : (a : M₂) → R)
              ((b₂ : (a : m) → M₂) j : M₂) :
            R))
    0
Tactic: rw [Finsupp.sum_fintype]