-- Module: Mathlib.LinearAlgebra.Alternating.DomCoprod
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : MultilinearMap.{u_3, u_1, u_4, u_5} R' (fun (x : ιa) ↦ Mᵢ) N₁
b : MultilinearMap.{u_3, u_2, u_4, u_6} R' (fun (x : ιb) ↦ Mᵢ) N₂
simp_rw :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm ιa,
      ∑ x_1 : Perm ιb,
        (domCoprod' :
            (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
              MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
          (HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) x : ℤˣ)
            (HSMul.hSMul (α := ℤˣ) (β :=
              MultilinearMap.{u_3, u_1, u_4, u_5} R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R']
                MultilinearMap.{u_3, u_2, u_4, u_6} R' (fun (x : ιb) ↦ Mᵢ) N₂)
              (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) x_1 : ℤˣ)
              (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b))))
    (∑ x : Perm ιa,
      ∑ x_1 : Perm ιb,
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) x : ℤˣ)
          (HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
            (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) x_1 : ℤˣ)
            ((domCoprod' :
                  (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
                    MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b) :
              MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))))
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((domCoprod' :
          (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
            MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
        ((∑ σ : Perm ιa,
            HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) σ : ℤˣ) (domDomCongr σ a)) ⊗ₜ[R']
          ∑ σ : Perm ιb,
            HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) σ : ℤˣ) (domDomCongr σ b)) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm ιa,
        ∑ x_1 : Perm ιb,
          HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) x : ℤˣ)
            (HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
              (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) x_1 : ℤˣ)
              ((domCoprod' :
                    (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
                      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                  (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b) :
                MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))

Tactic:
simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, _root_.map_sum,
    ← TensorProduct.smul_tmul', TensorProduct.tmul_smul]

Premises used: TensorProduct.tmul_smul, map_sum, TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul'