-- Module: Mathlib.LinearAlgebra.Basis.Bilinear
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst : CommSemiring Rₗ
inst_1 : AddCommMonoid Mₗ
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : Module Rₗ Mₗ
inst_5 : Module Rₗ Nₗ
inst_6 : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
simp_rw :
  Eq.{u_13 + 1} (α := Pₗ)
    (Finsupp.sum ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x) fun (i : ι₁) (xi : Rₗ) ↦
        Finsupp.sum ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y) fun (j : ι₂) (yj : Rₗ) ↦
          xi •
            HSMul.hSMul (β := Pₗ) yj
              ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) i) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                  ((b₂' : (a : ι₂) → Nₗ) j : Nₗ) :
                Pₗ) :
      Pₗ)
    (((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] 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ₗ) → ι₂ →₀ Rₗ) y) fun (i : ι₂) (a : Rₗ) ↦
          HSMul.hSMul (β := Nₗ) a ((b₂' : (a : ι₂) → Nₗ) i : Nₗ)) :
      Pₗ)
simp_rw₁ :
  Eq.{u_13 + 1} (α := Pₗ)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
        ∑ x_2 ∈ Finsupp.support.{u_2, u_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
          HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ)
            ((((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ) : (a : ι₁) → Rₗ) x_1 : Rₗ)
            (HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ) (β := Pₗ)
              ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x_2 : Rₗ)
              ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) x_1) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                  ((b₂' : (a : ι₂) → Nₗ) x_2 : Nₗ) :
                Pₗ)) :
      Pₗ)
    (((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
            (∑ x_1 ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
              HSMul.hSMul.{u_10, u_11, u_11} (α := 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_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
          HSMul.hSMul.{u_10, u_12, u_12} (α := Rₗ) (β := Nₗ)
            ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x : Rₗ) ((b₂' : (a : ι₂) → Nₗ) x : Nₗ)) :
      Pₗ)
simp_rw₂ :
  Eq.{u_13 + 1} (α := Pₗ)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
        HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ)
          ((((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ) : (a : ι₁) → Rₗ) x_1 : Rₗ)
          (HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ) (β := Pₗ)
            ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x_2 : Rₗ)
            ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) x_1) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                ((b₂' : (a : ι₂) → Nₗ) x_2 : Nₗ) :
              Pₗ)))
    (∑ i ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
      (((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
              (HSMul.hSMul.{u_10, u_11, u_11} (α := Rₗ) (β := Mₗ)
                ((((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ) : (a : ι₁) → Rₗ) i : Rₗ)
                ((b₁' : (a : ι₁) → Mₗ) i : Mₗ)) :
            Nₗ →ₗ[Rₗ] Pₗ) :
          (a : Nₗ) → Pₗ)
        (∑ x ∈ Finsupp.support.{u_2, u_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
          HSMul.hSMul.{u_10, u_12, u_12} (α := Rₗ) (β := Nₗ)
            ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x : Rₗ) ((b₂' : (a : ι₂) → Nₗ) x : Nₗ)))
simp_rw₃ :
  Eq.{u_13 + 1} (α := Pₗ)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
        HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ)
          ((((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ) : (a : ι₁) → Rₗ) x_1 : Rₗ)
          (HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ) (β := Pₗ)
            ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x_2 : Rₗ)
            ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) x_1) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                ((b₂' : (a : ι₂) → Nₗ) x_2 : Nₗ) :
              Pₗ)))
    (∑ x_1 ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
        (((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
                (HSMul.hSMul.{u_10, u_11, u_11} (α := Rₗ) (β := Mₗ)
                  ((((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ) : (a : ι₁) → Rₗ) x_1 : Rₗ)
                  ((b₁' : (a : ι₁) → Mₗ) x_1 : Mₗ)) :
              Nₗ →ₗ[Rₗ] Pₗ) :
            (a : Nₗ) → Pₗ)
          (HSMul.hSMul.{u_10, u_12, u_12} (α := Rₗ) (β := Nₗ)
            ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x_2 : Rₗ)
            ((b₂' : (a : ι₂) → Nₗ) x_2 : Nₗ)))
simp_rw₄ :
  Eq.{u_13 + 1} (α := Pₗ)
    (∑ x_1 ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
        HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ)
          ((((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ) : (a : ι₁) → Rₗ) x_1 : Rₗ)
          (HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ) (β := Pₗ)
            ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x_2 : Rₗ)
            ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) x_1) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                ((b₂' : (a : ι₂) → Nₗ) x_2 : Nₗ) :
              Pₗ)))
    (∑ x_1 ∈ Finsupp.support.{u_1, u_10} (M := Rₗ) ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x),
      ∑ x_2 ∈ Finsupp.support.{u_2, u_10} (M := Rₗ) ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y),
        HSMul.hSMul.{u_10, u_13, u_13} (α := Rₗ) (β := Pₗ)
          ((((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ) : (a : ι₁) → Rₗ) x_1 : Rₗ)
          ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) x_1) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
              (HSMul.hSMul.{u_10, u_12, u_12} (α := Rₗ) (β := Nₗ)
                ((((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) : (a : ι₂) → Rₗ) x_2 : Rₗ)
                ((b₂' : (a : ι₂) → Nₗ) x_2 : Nₗ)) :
            Pₗ))
⊢ Eq.{u_13 + 1} (α := Pₗ)
    (Finsupp.sum ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x) fun (i : ι₁) (xi : Rₗ) ↦
        Finsupp.sum ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y) fun (j : ι₂) (yj : Rₗ) ↦
          xi •
            HSMul.hSMul (β := Pₗ) yj
              ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) i) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                  ((b₂' : (a : ι₂) → Nₗ) j : Nₗ) :
                Pₗ) :
      Pₗ)
    ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
              ((Finsupp.linearCombination Rₗ (⇑b₁' : (a : ι₁) → Mₗ) : (a : ι₁ →₀ Rₗ) → Mₗ)
                ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ)) :
            Nₗ →ₗ[Rₗ] Pₗ) :
          (a : Nₗ) → Pₗ)
        ((Finsupp.linearCombination Rₗ (⇑b₂' : (a : ι₂) → Nₗ) : (a : ι₂ →₀ Rₗ) → Nₗ)
            ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) :
          Nₗ) :
      Pₗ)

Tactic:
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smul₂, map_smul]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, map_sum, LinearMap.map_smul₂, LinearMap.map_sum₂, map_smul