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₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂
v : (i : ιa ⊕ ιb) → Mᵢ
H :
  HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂) =
    HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₂ : ℤˣ)
      (((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ⊗ₜ[R']
          (b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦ v ((σ₂ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
        N₁ ⊗[R'] N₂)
⊢ Eq (α := N₁ ⊗[R'] N₂)
    (((fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            σ₁ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        v :
      N₁ ⊗[R'] N₂)
    (((fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            σ₂ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        v :
      N₁ ⊗[R'] N₂)

Tactic:
simp only [MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply,
      coe_multilinearMap, MultilinearMap.smul_apply]

Premises used: MultilinearMap.smul_apply, MultilinearMap.domCoprod_apply, AlternatingMap.coe_multilinearMap, MultilinearMap.domDomCongr_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₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂
v : (i : ιa ⊕ ιb) → Mᵢ
⊢ σ₂ =
    HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
      ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))

Tactic:
replace h := inv_mul_eq_iff_eq_mul.mp h.symm
-- 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₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : (i : ιa ⊕ ιb) → Mᵢ
h :
  σ₂ =
    HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
      ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))
⊢ ((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
      (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
        ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))) =
    HMul.hMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ))

Tactic:
simp
-- 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₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : (i : ιa ⊕ ιb) → Mᵢ
h :
  σ₂ =
    HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
      ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))
⊢ ((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
      (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
        ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))) =
    HMul.hMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ))

Tactic:
have : Equiv.Perm.sign (σ₁ * Perm.sumCongrHom _ _ (sl, sr))
      = Equiv.Perm.sign σ₁ * (Equiv.Perm.sign sl * Equiv.Perm.sign sr) := by simp
-- 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₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
v : (i : ιa ⊕ ιb) → Mᵢ
h :
  σ₂ =
    HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
      ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))
this :
  ((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ)
      (HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
        ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb))) =
    HMul.hMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ₁ : ℤˣ)
      (HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ))
⊢ Eq (α := N₁ ⊗[R'] N₂)
    (HSMul.hSMul (α := ℤˣ) (β := N₁) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        ((a : (a : ιa → Mᵢ) → N₁)
            ((fun (i₁ : ιa) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))) ∘ (⇑sl : (a : ιa) → ιa)) :
          N₁) ⊗ₜ[R']
      HSMul.hSMul (α := ℤˣ) (β := N₂) (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ)
        ((b : (a : ιb → Mᵢ) → N₂)
            ((fun (i₂ : ιb) ↦ v ((σ₁ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))) ∘ (⇑sr : (a : ιb) → ιb)) :
          N₂))
    (HSMul.hSMul (α := ℤˣ) (β := N₁) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) sl : ℤˣ)
        ((a : (a : ιa → Mᵢ) → N₁) fun (i₁ : ιa) ↦
            v
              ((HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
                    ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb)) :
                  (a : ιa ⊕ ιb) → ιa ⊕ ιb)
                (Sum.inl i₁)) :
          N₁) ⊗ₜ[R']
      HSMul.hSMul (α := ℤˣ) (β := N₂) (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) sr : ℤˣ)
        ((b : (a : ιb → Mᵢ) → N₂) fun (i₂ : ιb) ↦
            v
              ((HMul.hMul (β := Perm (ιa ⊕ ιb)) σ₁
                    ((Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) : Perm (ιa ⊕ ιb)) :
                  (a : ιa ⊕ ιb) → ιa ⊕ ιb)
                (Sum.inr i₂)) :
          N₂))

Tactic:
simp only [Sum.map_inr, Perm.sumCongrHom_apply, Perm.sumCongr_apply, Sum.map_inl,
      Function.comp_def, Perm.coe_mul]

Premises used: Sum.map_inl, Equiv.Perm.coe_mul, Equiv.Perm.sumCongr_apply, Function.comp_def, Sum.map_inr, Equiv.Perm.sumCongrHom_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₂
σ : Perm (ιa ⊕ ιb)
⊢ summand a b (Quotient.mk'' σ) =
    HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
      (MultilinearMap.domDomCongr σ
        ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)))

Tactic:
rfl

Premises used: Quotient.liftOn', AlternatingMap.domCoprod.summand, 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₂
σ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
h :
  ∀ (a_1 : Perm (ιa ⊕ ιb)),
    HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
        ((summand a b (Quotient.mk'' a_1) : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂)
        ((summand a b (HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' a_1)) :
              (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
            v :
          N₁ ⊗[R'] N₂) =
      0
⊢ HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
      ((summand a b σ : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂)
      ((summand a b (swap i j • σ) : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂) =
    0

Tactic:
induction σ using Quotient.inductionOn'
-- 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
a_1 : Perm (ιa ⊕ ιb)
h :
  HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
      ((HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
              (MultilinearMap.domDomCongr a_1
                ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                  (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂)
      ((HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ)
                (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ) •
              MultilinearMap.domDomCongr (swap i j * a_1)
                ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                  (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂) =
    0
⊢ HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
      ((HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
              (MultilinearMap.domDomCongr a_1
                ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                  (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂)
      ((HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) (swap i j • a_1) : ℤˣ)
              (MultilinearMap.domDomCongr (swap i j • a_1)
                ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                  (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
rw [smul_eq_mul, Perm.sign_mul, Perm.sign_swap hij]

Premises used: Equiv.Perm.sign_mul, smul_eq_mul, Equiv.Perm.sign_swap
-- 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
a_1 : Perm (ιa ⊕ ιb)
h :
  HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
        ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
              v ((a_1 : (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_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
          N₁ ⊗[R'] N₂) +
      -HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂)
          (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
          ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
                v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (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 ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))) :
            N₁ ⊗[R'] N₂) =
    0
⊢ HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
      ((HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
              (MultilinearMap.domDomCongr a_1
                ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                  (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂)
      ((HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ)
                (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ) •
              MultilinearMap.domDomCongr (swap i j * a_1)
                ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                  (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂) =
    0

Tactic:
simp only [one_mul, neg_mul, Function.comp_apply, Units.neg_smul, Perm.coe_mul,
    MultilinearMap.smul_apply, MultilinearMap.neg_apply, MultilinearMap.domDomCongr_apply,
    MultilinearMap.domCoprod_apply]

Premises used: MultilinearMap.smul_apply, Equiv.Perm.coe_mul, Units.neg_smul, MultilinearMap.domCoprod_apply, MultilinearMap.neg_apply, Function.comp_apply, neg_mul, one_mul, MultilinearMap.domDomCongr_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
a_1 : Perm (ιa ⊕ ιb)
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
        ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
              v ((a_1 : (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_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
          N₁ ⊗[R'] N₂) +
      -HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂)
          (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
          ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
                v ((a_1 : (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_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
            N₁ ⊗[R'] N₂) =
    0

Tactic:
add_neg_cancel (G := N₁ ⊗[R'] N₂) _

Premises used: add_neg_cancel
-- 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
a_1 : Perm (ιa ⊕ ιb)
h :
  Eq (α := (i : ιa) → Mᵢ)
    (fun (i₁ : ιa) ↦ v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))))
    fun (i₁ : ιa) ↦ v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))
h₁ :
  Eq (α := (i : ιb) → Mᵢ)
    (fun (i₂ : ιb) ↦ v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))))
    fun (i₂ : ιb) ↦ v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
        ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
              v ((a_1 : (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_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂)) :
          N₁ ⊗[R'] N₂) +
      -HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂)
          (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a_1 : ℤˣ)
          ((((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) : (a : (i : ιa) → Mᵢ) → N₁) fun (i₁ : ιa) ↦
                v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (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 ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))) :
            N₁ ⊗[R'] N₂) =
    0

Tactic:
convert! add_neg_cancel (G := N₁ ⊗[R'] N₂) _ using 6

Premises used: add_neg_cancel
-- 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
a_1 : Perm (ιa ⊕ ιb)
h :
  ∀ (k : ιa),
    v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl k))) =
      v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl k))
⊢ Eq (α := (i : ιa) → Mᵢ)
    (fun (i₁ : ιa) ↦ v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))))
    fun (i₁ : ιa) ↦ v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i₁))

Tactic:
ext k
-- 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
a_1 : Perm (ιa ⊕ ιb)
k : ιa
h h₁ : v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl k)) = v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl k))
⊢ v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl k))) =
    v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl k))

Tactic:
rw [Equiv.apply_swap_eq_self hv]

Premises used: Equiv.apply_swap_eq_self
-- 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
a_1 : Perm (ιa ⊕ ιb)
h :
  ∀ (k : ιb),
    v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr k))) =
      v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr k))
⊢ Eq (α := (i : ιb) → Mᵢ)
    (fun (i₂ : ιb) ↦ v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))))
    fun (i₂ : ιb) ↦ v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i₂))

Tactic:
ext k
-- 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
a_1 : Perm (ιa ⊕ ιb)
k : ιb
h h₁ : v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr k)) = v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr k))
⊢ v ((swap i j : (a : ιa ⊕ ιb) → ιa ⊕ ιb) ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr k))) =
    v ((a_1 : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr k))

Tactic:
rw [Equiv.apply_swap_eq_self hv]

Premises used: Equiv.apply_swap_eq_self
-- 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₂
σ : Perm.ModSumCongr ιa ιb
v : ιa ⊕ ιb → Mᵢ
i j : ιa ⊕ ιb
hv : v i = v j
hij : i ≠ j
h :
  ∀ (σ : Perm (ιa ⊕ ιb)),
    HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' σ) = Quotient.mk'' σ →
      Eq (α := N₁ ⊗[R'] N₂) ((summand a b (Quotient.mk'' σ) : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂)
        (0 : N₁ ⊗[R'] N₂)
⊢ swap i j • σ = σ →
    Eq (α := N₁ ⊗[R'] N₂) ((summand a b σ : (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂) v : N₁ ⊗[R'] N₂) (0 : N₁ ⊗[R'] N₂)

Tactic:
induction σ using Quotient.inductionOn' with | _ σ