-- Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
theorem MultilinearMap.domCoprod_alternization [DecidableEq ιa] [DecidableEq ιb]
    (a : MultilinearMap R' (fun _ : ιa => Mᵢ) N₁) (b : MultilinearMap R' (fun _ : ιb => Mᵢ) N₂) :
    MultilinearMap.alternatization (MultilinearMap.domCoprod a b) =
      a.alternatization.domCoprod (MultilinearMap.alternatization b)

Proof state:
case a.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
⊢ ∑ y ∈ Finset.filter (fun x => x⁻¹ * σ ∈ (Perm.sumCongrHom ιa ιb).range) Finset.univ,
      Perm.sign y • domDomCongr y (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Tactic:
rw [← Finset.map_univ_equiv (Equiv.mulLeft σ), Finset.filter_map, Finset.sum_map]

Result:
case a.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
⊢ ∑
      x ∈
        Finset.filter ((fun x => x⁻¹ * σ ∈ (Perm.sumCongrHom ιa ιb).range) ∘ ⇑(Equiv.toEmbedding (Equiv.mulLeft σ)))
          Finset.univ,
      Perm.sign ((Equiv.toEmbedding (Equiv.mulLeft σ)) x) •
        domDomCongr ((Equiv.toEmbedding (Equiv.mulLeft σ)) x) (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Proof state:
case a.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
⊢ ∑ y ∈ Finset.filter (fun y => ⟦y⟧ = σ) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) σ

Tactic:
refine Quotient.inductionOn' σ fun σ => ?_

Result:
case a.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
⊢ ∑ y ∈ Finset.filter (fun y => ⟦y⟧ = Quotient.mk'' σ) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Proof state:
case a.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
⊢ ∑ x : Perm ιa × Perm ιb,
      Perm.sign (σ * (Perm.sumCongrHom ιa ιb) x) • domDomCongr (σ * (Perm.sumCongrHom ιa ιb) x) (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Tactic:
rw [domCoprod.summand_mk'', MultilinearMap.domCoprod_alternization_coe, ← Finset.sum_product',
  Finset.univ_product_univ, ← MultilinearMap.domDomCongrEquiv_apply, _root_.map_sum,
  Finset.smul_sum]

Result:
case a.e_f.h
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
⊢ ∑ x : Perm ιa × Perm ιb,
      Perm.sign (σ * (Perm.sumCongrHom ιa ιb) x) • domDomCongr (σ * (Perm.sumCongrHom ιa ιb) x) (a.domCoprod b) =
    ∑ x : Perm ιa × Perm ιb,
      Perm.sign σ •
        (domDomCongrEquiv σ) (Perm.sign x.1 • Perm.sign x.2 • (domDomCongr x.1 a).domCoprod (domDomCongr x.2 b))

Proof state:
case a.e_f.h.e_f.h.mk
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
al : Perm ιa
ar : Perm ιb
⊢ Perm.sign (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) •
      domDomCongr (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) (a.domCoprod b) =
    Perm.sign σ •
      (domDomCongrEquiv σ)
        (Perm.sign (al, ar).1 • Perm.sign (al, ar).2 • (domDomCongr (al, ar).1 a).domCoprod (domDomCongr (al, ar).2 b))

Tactic:
dsimp only

Result:
case a.e_f.h.e_f.h.mk
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : MultilinearMap R' (fun x => Mᵢ) N₁
b : MultilinearMap R' (fun x => Mᵢ) N₂
σ✝ : Quotient (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)
σ : Perm (ιa ⊕ ιb)
al : Perm ιa
ar : Perm ιb
⊢ Perm.sign (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) •
      domDomCongr (σ * (Perm.sumCongrHom ιa ιb) (al, ar)) (a.domCoprod b) =
    Perm.sign σ • (domDomCongrEquiv σ) (Perm.sign al • Perm.sign ar • (domDomCongr al a).domCoprod (domDomCongr ar b))