-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Bilinear (goal)
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
simp_rw :
  Eq.{u_9 + 1} (α := P)
    (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
        Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
          HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
            (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
              ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                  ((b₂ : (a : ι₂) → N) j : N) :
                P)) :
      P)
    (((B : (a : M) → N →ₛₗ[σ₁₂] P)
            (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (a : R) ↦
              HSMul.hSMul (β := M) a ((b₁ : (a : ι₁) → M) i : M)) :
          (a : N) → P)
        (Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (i : ι₂) (a : S) ↦
          HSMul.hSMul (β := N) a ((b₂ : (a : ι₂) → N) i : N)) :
      P)
simp_rw₁ :
  Eq.{u_9 + 1} (α := P)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
        ∑ x_2 ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
          HSMul.hSMul.{u_4, u_9, u_9} (α := R₂)
            ((ρ₁₂ : (a : R) → R₂) ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) x_1 : R) : R₂)
            (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P)
              ((σ₁₂ : (a : S) → S₂) ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x_2 : S) : S₂)
              ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) x_1) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                  ((b₂ : (a : ι₂) → N) x_2 : N) :
                P)) :
      P)
    (((B : (a : M) → N →ₛₗ[σ₁₂] P)
            (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
              HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := M)
                ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) x_1 : R) ((b₁ : (a : ι₁) → M) x_1 : M)) :
          (a : N) → P)
        (∑ x ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
          HSMul.hSMul.{u_5, u_8, u_8} (α := S) (β := N)
            ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x : S) ((b₂ : (a : ι₂) → N) x : N)) :
      P)
simp_rw₂ :
  Eq.{u_9 + 1} (α := P)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
        HSMul.hSMul.{u_4, u_9, u_9} (α := R₂)
          ((ρ₁₂ : (a : R) → R₂) ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) x_1 : R) : R₂)
          (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P)
            ((σ₁₂ : (a : S) → S₂) ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x_2 : S) : S₂)
            ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) x_1) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                ((b₂ : (a : ι₂) → N) x_2 : N) :
              P)))
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
      (((B : (a : M) → N →ₛₗ[σ₁₂] P)
              (HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := M)
                ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) i : R) ((b₁ : (a : ι₁) → M) i : M)) :
            N →ₛₗ[σ₁₂] P) :
          (a : N) → P)
        (∑ x ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
          HSMul.hSMul.{u_5, u_8, u_8} (α := S) (β := N)
            ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x : S) ((b₂ : (a : ι₂) → N) x : N)))
simp_rw₃ :
  Eq.{u_9 + 1} (α := P)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
        HSMul.hSMul.{u_4, u_9, u_9} (α := R₂)
          ((ρ₁₂ : (a : R) → R₂) ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) x_1 : R) : R₂)
          (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P)
            ((σ₁₂ : (a : S) → S₂) ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x_2 : S) : S₂)
            ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) x_1) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                ((b₂ : (a : ι₂) → N) x_2 : N) :
              P)))
    (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
        (((B : (a : M) → N →ₛₗ[σ₁₂] P)
                (HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := M)
                  ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) x_1 : R)
                  ((b₁ : (a : ι₁) → M) x_1 : M)) :
              N →ₛₗ[σ₁₂] P) :
            (a : N) → P)
          (HSMul.hSMul.{u_5, u_8, u_8} (α := S) (β := N)
            ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x_2 : S) ((b₂ : (a : ι₂) → N) x_2 : N)))
⊢ Eq.{u_9 + 1} (α := P)
    (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
        Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
          HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
            (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
              ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                  ((b₂ : (a : ι₂) → N) j : N) :
                P)) :
      P)
    ((((B : (a : M) → N →ₛₗ[σ₁₂] P)
              ((Finsupp.linearCombination R (⇑b₁ : (a : ι₁) → M) : (a : ι₁ →₀ R) → M)
                ((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R)) :
            N →ₛₗ[σ₁₂] P) :
          (a : N) → P)
        ((Finsupp.linearCombination S (⇑b₂ : (a : ι₂) → N) : (a : ι₂ →₀ S) → N)
            ((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) :
          N) :
      P)
have simp_rw₄ : Eq.{u_9 + 1} (α := P)
  (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
    ∑ x_2 ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
      HSMul.hSMul.{u_4, u_9, u_9} (α := R₂)
        ((ρ₁₂ : (a : R) → R₂) ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) x_1 : R) : R₂)
        (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P)
          ((σ₁₂ : (a : S) → S₂) ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x_2 : S) : S₂)
          ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) x_1) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
              ((b₂ : (a : ι₂) → N) x_2 : N) :
            P)))
  (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b₁.repr : (a : M) → ι₁ →₀ R) x),
    ∑ x_2 ∈ Finsupp.support.{u_2, u_5} (M := S) ((b₂.repr : (a : N) → ι₂ →₀ S) y),
      HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) (β := P)
        ((ρ₁₂ : (a : R) → R₂) ((((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R) : (a : ι₁) → R) x_1 : R) : R₂)
        ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) x_1) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
            (HSMul.hSMul.{u_5, u_8, u_8} (α := S) (β := N)
              ((((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) : (a : ι₂) → S) x_2 : S) ((b₂ : (a : ι₂) → N) x_2 : N)) :
          P))
Tactic: simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smulₛₗ₂, map_smulₛₗ]