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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' : ιb
j' : ιa
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          ((↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) : (a : (i : ιb) → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
case inr.inl => simpa using Equiv.congr_fun hσ (Sum.inr i')

Premises used: Equiv.congr_fun, Sum.inr
-- 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₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιa
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
this :
  Eq.{u_5 + 1} (α := N₁) ((a : (a : ιa → Mᵢ) → N₁) fun (i : ιa) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i)) : N₁)
    (0 : N₁)
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          ((↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) : (a : (i : ιb) → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
simp_all
-- 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₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιa
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
suffices :
  Eq.{u_5 + 1} (α := N₁) ((a : (a : ιa → Mᵢ) → N₁) fun (i : ιa) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i)) : N₁)
    (0 : N₁)
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          ((↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) : (a : (i : ιb) → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
suffices (a fun i ↦ v (σ (Sum.inl i))) = 0 by simp_all
-- 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₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιa
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
⊢ Eq.{u_5 + 1} (α := N₁) ((a : (a : ιa → Mᵢ) → N₁) fun (i : ιa) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i)) : N₁)
    (0 : N₁)

Tactic:
AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)

Premises used: Eq.rec, AlternatingMap.map_eq_zero_of_eq, 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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιa
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
⊢ Eq.{u_5 + 1} (α := N₁) ((a : (a : ιa → Mᵢ) → N₁) fun (i : ιa) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i)) : N₁)
    (0 : N₁)

Tactic:
exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)

Premises used: Eq.rec, AlternatingMap.map_eq_zero_of_eq, 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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιa
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          ((↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) : (a : (i : ιb) → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
case inl.inl =>
    suffices (a fun i ↦ v (σ (Sum.inl i))) = 0 by simp_all
    exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)

Premises used: Eq.rec, AlternatingMap.map_eq_zero_of_eq, 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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιb
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
this :
  Eq.{u_6 + 1} (α := N₂) ((b : (a : ιb → Mᵢ) → N₂) fun (i : ιb) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i)) : N₂)
    (0 : N₂)
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          ((↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) : (a : (i : ιb) → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
simp_all
-- 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₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιb
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
suffices :
  Eq.{u_6 + 1} (α := N₂) ((b : (a : ιb → Mᵢ) → N₂) fun (i : ιb) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i)) : N₂)
    (0 : N₂)
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          ((↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) : (a : (i : ιb) → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
suffices (b fun i ↦ v (σ (Sum.inr i))) = 0 by simp_all
-- 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₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιb
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
⊢ Eq.{u_6 + 1} (α := N₂) ((b : (a : ιb → Mᵢ) → N₂) fun (i : ιb) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i)) : N₂)
    (0 : N₂)

Tactic:
b.map_eq_zero_of_eq _ hv fun hij' => hij (hij' ▸ rfl)

Premises used: Eq.rec, AlternatingMap.map_eq_zero_of_eq, 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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιb
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
⊢ Eq.{u_6 + 1} (α := N₂) ((b : (a : ιb → Mᵢ) → N₂) fun (i : ιb) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i)) : N₂)
    (0 : N₂)

Tactic:
exact b.map_eq_zero_of_eq _ hv fun hij' => hij (hij' ▸ 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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
σ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
i' j' : ιb
hv : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j'))
hij :
  Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i') : ιa ⊕ ιb)
    ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j') : ιa ⊕ ιb)
hσ_1 :
  HSMul.hSMul (α := Perm (ιa ⊕ ιb)) (β := Perm.ModSumCongr ιa ιb)
      (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) : Perm (ιa ⊕ ιb))
      (Quotient.mk'' σ) =
    Quotient.mk'' σ
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := Perm (ιa ⊕ ιb))
              (swap ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')) :
                Perm (ιa ⊕ ιb))
              x)
          σ)⁻¹ *
      σ
case case₁ case₂ :
  Eq.{u_6 + 1} (α := N₂) ((b : (a : ιb → Mᵢ) → N₂) fun (i : ιb) ↦ v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i)) : N₂)
    (0 : N₂)
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          ((↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) : (a : (i : ιb) → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
case inr.inr =>
    suffices (b fun i ↦ v (σ (Sum.inr i))) = 0 by simp_all
    exact b.map_eq_zero_of_eq _ hv fun hij' => hij (hij' ▸ 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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
rw :
  Eq (α := N₁ ⊗[R'] N₂)
    (∑ a_1 : Perm.ModSumCongr ιa ιb, (domCoprod.summand a b a_1 : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v) 0
⊢ Eq (α := N₁ ⊗[R'] N₂)
    ((∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂)
    (0 : N₁ ⊗[R'] N₂)

Tactic:
rw [MultilinearMap.sum_apply]

Premises used: MultilinearMap.sum_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 : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ Eq (α := N₁ ⊗[R'] N₂)
    (∑ a_1 : Perm.ModSumCongr ιa ιb, (domCoprod.summand a b a_1 : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v) 0

Tactic:
Finset.sum_involution (fun σ _ => Equiv.swap i j • σ)
          (fun σ _ => domCoprod.summand_add_swap_smul_eq_zero a b σ hv hij)
          (fun σ _ => mt <| domCoprod.summand_eq_zero_of_smul_invariant a b σ hv hij)
          (fun σ _ => Finset.mem_univ _) fun σ _ =>
          Equiv.swap_smul_involutive i j σ

Premises used: Finset.mem_univ, Equiv.swap_smul_involutive, Equiv.swap, mt, AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant, HSMul.hSMul, Finset.sum_involution, AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero
-- 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₂
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
⊢ Eq (α := N₁ ⊗[R'] N₂)
    (∑ a_1 : Perm.ModSumCongr ιa ιb, (domCoprod.summand a b a_1 : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v) 0

Tactic:
exact
        Finset.sum_involution (fun σ _ => Equiv.swap i j • σ)
          (fun σ _ => domCoprod.summand_add_swap_smul_eq_zero a b σ hv hij)
          (fun σ _ => mt <| domCoprod.summand_eq_zero_of_smul_invariant a b σ hv hij)
          (fun σ _ => Finset.mem_univ _) fun σ _ =>
          Equiv.swap_smul_involutive i j σ

Premises used: Finset.mem_univ, Equiv.swap_smul_involutive, Equiv.swap, mt, AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant, HSMul.hSMul, Finset.sum_involution, AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero