-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Hom (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_9
b : Basis ι R M
x y : M
simp_rw :
  Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (xi : R) ↦
        Finsupp.sum ((b.repr : (a : M) → ι →₀ R) y) fun (j : ι) (yj : R) ↦
          xi •
            HSMul.hSMul (β := R) yj
              ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) :
                R) :
      R)
    (((B : (a : M) → M →ₗ[R] R)
            (Finsupp.sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (a : R) ↦
              HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) :
          (a : M) → R)
        (Finsupp.sum ((b.repr : (a : M) → ι →₀ R) y) fun (i : ι) (a : R) ↦
          HSMul.hSMul (β := M) a ((b : (a : ι) → M) i : M)) :
      R)
simp_rw₁ :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
        ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
          HSMul.hSMul (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
            (HSMul.hSMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R)
              ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R)
                  ((b : (a : ι) → M) x_2 : M) :
                R)) :
      R)
    (((B : (a : M) → M →ₗ[R] R)
            (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
                ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → M) x_1 : M)) :
          (a : M) → R)
        (∑ x ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x : R)
            ((b : (a : ι) → M) x : M)) :
      R)
simp_rw₂ :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
        HSMul.hSMul (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          (HSMul.hSMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R)
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R)
                ((b : (a : ι) → M) x_2 : M) :
              R)))
    (∑ i ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
      (((B : (a : M) → M →ₗ[R] R)
              (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
                ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((b : (a : ι) → M) i : M)) :
            M →ₗ[R] R) :
          (a : M) → R)
        (∑ x ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x : R)
            ((b : (a : ι) → M) x : M)))
simp_rw₃ :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
        HSMul.hSMul (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          (HSMul.hSMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R)
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R)
                ((b : (a : ι) → M) x_2 : M) :
              R)))
    (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
      ∑ i ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
        (((B : (a : M) → M →ₗ[R] R)
                (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
                  ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → M) x_1 : M)) :
              M →ₗ[R] R) :
            (a : M) → R)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
            ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R) ((b : (a : ι) → M) i : M)))
simp_rw₄ :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
        HSMul.hSMul (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          (HSMul.hSMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R)
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R)
                ((b : (a : ι) → M) x_2 : M) :
              R)))
    (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
        HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
          ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R)
              (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
                ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R) ((b : (a : ι) → M) x_2 : M)) :
            R))
⊢ Eq.{u_1 + 1} (α := R)
    (Finsupp.sum ((b.repr : (a : M) → ι →₀ R) x) fun (i : ι) (xi : R) ↦
        Finsupp.sum ((b.repr : (a : M) → ι →₀ R) y) fun (j : ι) (yj : R) ↦
          xi •
            HSMul.hSMul (β := R) yj
              ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) :
                R) :
      R)
    ((((B : (a : M) → M →ₗ[R] R)
              ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M)
                ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R)) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Finsupp.linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) :
          M) :
      R)
have simp_rw₅ : Eq.{u_1 + 1} (α := R)
  (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
    ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
      HSMul.hSMul (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
        (HSMul.hSMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R)
          ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) x_2 : M) :
            R)))
  (∑ x_1 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
    ∑ x_2 ∈ Finsupp.support.{u_9, u_1} (M := R) ((b.repr : (a : M) → ι →₀ R) y),
      HMul.hMul (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R)
        (HMul.hMul (α := R) (β := R) ((((b.repr : (a : M) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x_2 : R)
          ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) x_1) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) x_2 : M) :
            R)))
Tactic: simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, sum_left, sum_right, smul_left, smul_right,
    smul_eq_mul]