-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
τ :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ τ : Perm (ιa ⊕ ιb) with ⟦τ⟧ = Quotient.mk'' σ,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) τ : ℤˣ)
        (domDomCongr τ (a.domCoprod b)))
    (∑ τ : Perm (ιa ⊕ ιb) with τ⁻¹ * σ ∈ f.range,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) τ : ℤˣ)
        (domDomCongr τ (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 ⊕ ιb) with τ⁻¹ ∈ f.range,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (σ * τ) : ℤˣ)
        (domDomCongr (σ * τ) (a.domCoprod b)))
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = Quotient.mk'' σ,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) y : ℤˣ)
        (domDomCongr y (a.domCoprod b)))
    (domCoprod.summand ((alternatization : (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) → Mᵢ [⋀^ιa]→ₗ[R'] N₁) a)
      ((alternatization : (a : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) → Mᵢ [⋀^ιb]→ₗ[R'] N₂) b) (Quotient.mk'' σ))
have τ₂ : 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: calc
    ∑ τ ∈ _, sign τ • domDomCongr τ (a.domCoprod b) =
        ∑ τ ∈ {τ | τ⁻¹ * σ ∈ f.range}, sign τ • domDomCongr τ (a.domCoprod b) := by
      simp [QuotientGroup.leftRel_apply, f, Quotient.eq]
    _ = ∑ τ ∈ {τ | τ⁻¹ ∈ f.range}, sign (σ * τ) • domDomCongr (σ * τ) (a.domCoprod b) := by
      conv_lhs => rw [← Finset.map_univ_equiv (Equiv.mulLeft σ), Finset.filter_map, Finset.sum_map]
      simp [-MonoidHom.mem_range]
    _ = ∑ τ, sign (σ * f τ) • domDomCongr (σ * f τ) (a.domCoprod b) := by
      simp_rw [f, Subgroup.inv_mem_iff, MonoidHom.mem_range, Finset.univ_filter_exists,
        Finset.sum_image sumCongrHom_injective.injOn]
    _ = ∑ τ : Perm ιa × Perm ιb,
         sign σ • (domDomCongrEquiv σ) (sign τ.1 • sign τ.2 •
           (domDomCongr τ.1 a).domCoprod (domDomCongr τ.2 b)) := by
      simp [f, domDomCongr_mul, domCoprod_domDomCongr_sumCongr, mul_smul]
    _ = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ) := by
      simp [domCoprod.summand_mk'', domCoprod_alternization_coe, ← domDomCongrEquiv_apply,
        Finset.smul_sum, ← Finset.sum_product']