-- 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 y => ⟦y⟧ = Quotient.mk'' σ) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Tactic:
rw
  [@Finset.filter_congr _ _ _ (fun a => @Quotient.decidableEq _ _
    (QuotientGroup.leftRelDecidable (MonoidHom.range (Perm.sumCongrHom ιa ιb)))
    (Quotient.mk (QuotientGroup.leftRel (MonoidHom.range (Perm.sumCongrHom ιa ιb))) a)
    (Quotient.mk'' σ)) _ (s := Finset.univ)
  fun x _ => QuotientGroup.eq (s := MonoidHom.range (Perm.sumCongrHom ιa ιb)) (a := x) (b := σ)]

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 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'' σ)

Proof state:
case a
ι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₂
⊢ ∑ xbar ∈ Finset.image (Quotient.mk (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)) Finset.univ,
      ∑ y ∈ Finset.filter (fun y => ⟦y⟧ = xbar) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b) =
    ∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand (alternatization a) (alternatization b) σ

Tactic:
congr 1

Result:
case a.e_f
ι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₂
⊢ (fun xbar => ∑ y ∈ Finset.filter (fun y => ⟦y⟧ = xbar) Finset.univ, Perm.sign y • domDomCongr y (a.domCoprod b)) =
    fun σ => domCoprod.summand (alternatization a) (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)
⊢ ∑
      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'' σ)

Tactic:
simp_rw [Equiv.coe_toEmbedding, Equiv.coe_mulLeft, Function.comp_def, mul_inv_rev,
  inv_mul_cancel_right, Subgroup.inv_mem_iff, MonoidHom.mem_range, Finset.univ_filter_exists,
  Finset.sum_image Perm.sumCongrHom_injective.injOn]

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) =
    domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ)

Proof state:
case a.e_f.h.e_f
ι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)
⊢ (fun x => Perm.sign (σ * (Perm.sumCongrHom ιa ιb) x) • domDomCongr (σ * (Perm.sumCongrHom ιa ιb) x) (a.domCoprod b)) =
    fun x =>
    Perm.sign σ •
      (domDomCongrEquiv σ) (Perm.sign x.1 • Perm.sign x.2 • (domDomCongr x.1 a).domCoprod (domDomCongr x.2 b))

Tactic:
ext1 ⟨al, ar⟩

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, ar).1 • Perm.sign (al, ar).2 • (domDomCongr (al, ar).1 a).domCoprod (domDomCongr (al, ar).2 b))