awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm ιa,
      ∑ x_1 : Perm ιb,
        (domCoprod' :
            (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
              MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
          (HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) x : ℤˣ)
            (HSMul.hSMul (α := ℤˣ) (β :=
              MultilinearMap.{u_3, u_1, u_4, u_5} R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R']
                MultilinearMap.{u_3, u_2, u_4, u_6} R' (fun (x : ιb) ↦ Mᵢ) N₂)
              (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) x_1 : ℤˣ)
              (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b))))
    (∑ x : Perm ιa,
      ∑ x_1 : Perm ιb,
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) x : ℤˣ)
          (HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
            (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) x_1 : ℤˣ)
            ((domCoprod' :
                  (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
                    MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b) :
              MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))))

Tactic:
rfl
-- 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₂
a₁ :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (↑((alternatization :
            (a : MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
          (a.domCoprod b)) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (↑(AlternatingMap.domCoprod
          ((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)) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
⊢ Eq (α := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
    ((alternatization :
          (a : MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
        (a.domCoprod b) :
      Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
    (AlternatingMap.domCoprod
        ((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) :
      Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)

Tactic:
apply coe_multilinearMap_injective

Premises used: AlternatingMap.coe_multilinearMap_injective
-- 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₂
a₁ :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ xbar ∈ Finset.image (Quotient.mk (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)) Finset.univ,
      ∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = xbar,
        HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) y : ℤˣ)
          (domDomCongr y (a.domCoprod b)))
    (∑ σ : ModSumCongr ιa ι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) σ)
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (↑((alternatization :
            (a : MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
          (a.domCoprod b)) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (↑(AlternatingMap.domCoprod
          ((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)) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))

Tactic:
rw [domCoprod_coe, MultilinearMap.alternatization_coe,
    Finset.sum_partition (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range)]

Premises used: MonoidHom.range, Equiv.Perm.sumCongrHom, AlternatingMap.domCoprod_coe, QuotientGroup.leftRel, MultilinearMap.alternatization_coe, Finset.sum_partition
-- 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₂
a₁ :
  Eq (α :=
    Quotient (QuotientGroup.leftRel (sumCongrHom ιa ιb).range) →
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (fun (xbar : Quotient (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)) ↦
      ∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = xbar,
        HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) y : ℤˣ)
          (domDomCongr y (a.domCoprod b)))
    fun (σ : ModSumCongr ιa ι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) σ
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ xbar ∈ Finset.image (Quotient.mk (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)) Finset.univ,
      ∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = xbar,
        HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) y : ℤˣ)
          (domDomCongr y (a.domCoprod b)))
    (∑ σ : ModSumCongr ιa ι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) σ)

Tactic:
congr 1
-- 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₂
a₁ :
  ∀ (σ : Quotient (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)),
    Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
      (∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = σ,
        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) σ)
⊢ Eq (α :=
    Quotient (QuotientGroup.leftRel (sumCongrHom ιa ιb).range) →
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (fun (xbar : Quotient (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)) ↦
      ∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = xbar,
        HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) y : ℤˣ)
          (domDomCongr y (a.domCoprod b)))
    fun (σ : ModSumCongr ιa ι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) σ

Tactic:
ext1 σ
-- 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
⊢ 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)))

Tactic:
simp [QuotientGroup.leftRel_apply, f, Quotient.eq]

Premises used: Quotient.eq, QuotientGroup.leftRel_apply
-- 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
rw :
  ∑ x : Perm (ιa ⊕ ιb) with
    ((fun (τ : Perm (ιa ⊕ ιb)) ↦ τ⁻¹ * σ ∈ f.range) ∘
        (⇑(Equiv.toEmbedding (Equiv.mulLeft σ)) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)))
      x,
    HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
      (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
          ((Equiv.toEmbedding (Equiv.mulLeft σ) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)) x) :
        ℤˣ)
      (domDomCongr ((Equiv.toEmbedding (Equiv.mulLeft σ) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)) x) (a.domCoprod b))
| ∑ τ : Perm (ιa ⊕ ιb) with τ⁻¹ * σ ∈ f.range,
    HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) τ : ℤˣ)
      (domDomCongr τ (a.domCoprod b))

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

Premises used: Finset.sum_map, Finset.map_univ_equiv, Equiv.mulLeft, Finset.filter_map
-- 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
conv_lhs :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm (ιa ⊕ ιb) with
      ((fun (τ : Perm (ιa ⊕ ιb)) ↦ τ⁻¹ * σ ∈ f.range) ∘
          (⇑(Equiv.toEmbedding (Equiv.mulLeft σ)) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)))
        x,
      HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
            ((Equiv.toEmbedding (Equiv.mulLeft σ) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)) x) :
          ℤˣ)
        (domDomCongr ((Equiv.toEmbedding (Equiv.mulLeft σ) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)) x) (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)))

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

Premises used: Finset.sum_map, Finset.map_univ_equiv, Equiv.mulLeft, Finset.filter_map
-- 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
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm (ιa ⊕ ιb) with
      ((fun (τ : Perm (ιa ⊕ ιb)) ↦ τ⁻¹ * σ ∈ f.range) ∘
          (⇑(Equiv.toEmbedding (Equiv.mulLeft σ)) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)))
        x,
      HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
            ((Equiv.toEmbedding (Equiv.mulLeft σ) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)) x) :
          ℤˣ)
        (domDomCongr ((Equiv.toEmbedding (Equiv.mulLeft σ) : (a : Perm (ιa ⊕ ιb)) → Perm (ιa ⊕ ιb)) x) (a.domCoprod b)))
    (∑ τ : Perm (ιa ⊕ ιb) with τ⁻¹ ∈ f.range,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (σ * τ) : ℤˣ)
        (domDomCongr (σ * τ) (a.domCoprod b)))

Tactic:
simp [-MonoidHom.mem_range]

Premises used: MonoidHom.mem_range
-- 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
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ τ : 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)))
    (∑ τ : Perm ιa × Perm ιb,
      HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
        ((domDomCongrEquiv σ :
              (a : MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) →
                MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
            (HSMul.hSMul (α := ℤˣ) (((sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) τ.1 : ℤˣ)
              (HSMul.hSMul (α := ℤˣ) (((sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) τ.2 : ℤˣ)
                ((domDomCongr τ.1 a).domCoprod (domDomCongr τ.2 b)))) :
          MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)))

Tactic:
simp [f, domDomCongr_mul, domCoprod_domDomCongr_sumCongr, mul_smul]

Premises used: MultilinearMap.domCoprod_domDomCongr_sumCongr, MultilinearMap.domDomCongr_mul, SemigroupAction.mul_smul
-- 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
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ τ : Perm ιa × Perm ιb,
      HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
        (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
        ((domDomCongrEquiv σ :
              (a : MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) →
                MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
            (HSMul.hSMul (α := ℤˣ) (((sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) τ.1 : ℤˣ)
              (HSMul.hSMul (α := ℤˣ) (((sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) τ.2 : ℤˣ)
                ((domDomCongr τ.1 a).domCoprod (domDomCongr τ.2 b)))) :
          MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)))
    (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'' σ))

Tactic:
simp [domCoprod.summand_mk'', domCoprod_alternization_coe, ← domDomCongrEquiv_apply,
        Finset.smul_sum, ← Finset.sum_product']

Premises used: AlternatingMap.domCoprod.summand_mk'', MultilinearMap.domCoprod_alternization_coe, Finset.sum_product', Finset.smul_sum, MultilinearMap.domDomCongrEquiv_apply
-- 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₂
σ : Quotient (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)
a₁ :
  ∀ (σ : Perm (ιa ⊕ ι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'' σ))
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = σ,
      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) σ)

Tactic:
induction σ using Quotient.inductionOn' with
  | h σ =>
  set f := sumCongrHom ιa ιb
  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']

Premises used: Equiv.Perm.sumCongrHom, Equiv.Perm
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
rw :
  HSMul.hSMul (α := ℤˣ) (β := N) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (n + 1))) → ℤˣ) p.cycleRange : ℤˣ)
      ((f : (a : Fin (n + 1) → M) → N) (cons (α := fun (a : Fin (n + 1)) ↦ M) x v) : N) =
    HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ))
      ((f : (a : Fin (n + 1) → M) → N) (cons (α := fun (a : Fin n.succ) ↦ M) x v) : N)
⊢ (f : (a : Fin (n + 1) → M) → N) (p.insertNth (α := fun (a : Fin (n + 1)) ↦ M) x v) =
    HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ)) ((f : (a : Fin (n + 1) → M) → N) (Matrix.vecCons x v) : N)

Tactic:
rw [← cons_comp_cycleRange, map_perm, Matrix.vecCons]

Premises used: AlternatingMap.map_perm, Matrix.vecCons, Fin.cons_comp_cycleRange
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ HSMul.hSMul (α := ℤˣ) (β := N) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (n + 1))) → ℤˣ) p.cycleRange : ℤˣ)
      ((f : (a : Fin (n + 1) → M) → N) (cons (α := fun (a : Fin (n + 1)) ↦ M) x v) : N) =
    HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ))
      ((f : (a : Fin (n + 1) → M) → N) (cons (α := fun (a : Fin n.succ) ↦ M) x v) : N)

Tactic:
simp [Units.smul_def]

Premises used: Units.smul_def