-- 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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : (i : ιa ⊕ ιb) → Mᵢ
h :
  σ₂ =
    HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
      ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))
this :
  ((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
      (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
        ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))) =
    HMul.hMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ))
H :
  Eq (α := N₁ ⊗[R'] N₂)
    (HSMul.hSMul (α := ℤˣ) (β := N₁) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        ((a : (a : ιa → Mᵢ) → N₁)
            ((fun (i₁ : ιa) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ∘ (⇑sl : (a : ιa) → ιa)) :
          N₁) ⊗ₜ[R']
      HSMul.hSMul (α := ℤˣ) (β := N₂) (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ)
        ((b : (a : ιb → Mᵢ) → N₂)
            ((fun (i₂ : ιb) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))) ∘ (⇑sr : (a : ιb) → ιb)) :
          N₂))
    (HSMul.hSMul (α := ℤˣ) (β := N₁) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        ((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v
              ((HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
                    ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb)) :
                  (a : ιa ⊕ ιb) → ιa ⊕ ιb)
                (Sum.inl i₁)) :
          N₁) ⊗ₜ[R']
      HSMul.hSMul (α := ℤˣ) (β := N₂) (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ)
        ((b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v
              ((HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
                    ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb)) :
                  (a : ιa ⊕ ιb) → ιa ⊕ ιb)
                (Sum.inr i₂)) :
          N₂))
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₂ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂)

Tactic:
rw [h, this, mul_smul, mul_smul, smul_left_cancel_iff, ← TensorProduct.tmul_smul,
      TensorProduct.smul_tmul', a.map_congr_perm _ sl, b.map_congr_perm _ sr]

Premises used: AlternatingMap.map_congr_perm, TensorProduct.tmul_smul, TensorProduct.smul_tmul', SemigroupAction.mul_smul, smul_left_cancel_iff