-- 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₂
σ : Perm (ιa ⊕ ιb)
f : Prod.{u_1, u_2} (Perm ιa) (Perm ιb) →* Perm (ιa ⊕ ιb) := sumCongrHom ιa ιb
simp_rw :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm (ιa ⊕ ιb) with x⁻¹ ∈ (sumCongrHom ιa ιb).range,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (σ * x) : ℤˣ)
        (domDomCongr (σ * x) (a.domCoprod b)))
    (∑ x : Perm ιa × Perm ιb,
      HSMul.hSMul (α := ℤˣ)
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
            (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
              ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb))) :
          ℤˣ)
        (domDomCongr
          (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
            ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb)))
          (a.domCoprod b)))
simp_rw₁ :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm (ιa ⊕ ιb) with x ∈ (sumCongrHom ιa ιb).range,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (σ * x) : ℤˣ)
        (domDomCongr (σ * x) (a.domCoprod b)))
    (∑ x : Perm ιa × Perm ιb,
      HSMul.hSMul (α := ℤˣ)
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
            (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
              ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb))) :
          ℤˣ)
        (domDomCongr
          (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
            ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb)))
          (a.domCoprod b)))
simp_rw₂ :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm (ιa ⊕ ιb) with
      ∃ (x_1 : Prod.{u_1, u_2} (Perm ιa) (Perm ιb)),
        (sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x_1 = x,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (σ * x) : ℤˣ)
        (domDomCongr (σ * x) (a.domCoprod b)))
    (∑ x : Perm ιa × Perm ιb,
      HSMul.hSMul (α := ℤˣ)
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
            (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
              ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb))) :
          ℤˣ)
        (domDomCongr
          (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
            ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb)))
          (a.domCoprod b)))
simp_rw₃ :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑
      x ∈
        Finset.image (α := Prod.{u_1, u_2} (Perm ιa) (Perm ιb))
          (⇑(sumCongrHom ιa ιb) : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) Finset.univ,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (σ * x) : ℤˣ)
        (domDomCongr (σ * x) (a.domCoprod b)))
    (∑ x : Perm ιa × Perm ιb,
      HSMul.hSMul (α := ℤˣ)
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
            (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
              ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb))) :
          ℤˣ)
        (domDomCongr
          (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ
            ((sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) x : Perm (ιa ⊕ ιb)))
          (a.domCoprod b)))
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ τ : Perm (ιa ⊕ ιb) with τ⁻¹ ∈ f.range,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (σ * τ) : ℤˣ)
        (domDomCongr (σ * τ) (a.domCoprod b)))
    (∑ τ : Perm ιa × Perm ιb,
      HSMul.hSMul (α := ℤˣ)
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
            (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ ((f : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) τ : Perm (ιa ⊕ ιb))) :
          ℤˣ)
        (domDomCongr
          (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ ((f : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) τ : Perm (ιa ⊕ ιb)))
          (a.domCoprod b)))

Tactic:
simp_rw [f, Subgroup.inv_mem_iff, MonoidHom.mem_range, Finset.univ_filter_exists,
        Finset.sum_image sumCongrHom_injective.injOn]

Premises used: Finset.univ_filter_exists, Function.Injective.injOn, MonoidHom.mem_range, Equiv.Perm.sumCongrHom_injective, Subgroup.inv_mem_iff, Finset.sum_image