awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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)
⊢ 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
have 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
Tactic: rw [smul_eq_mul, Perm.sign_mul, Perm.sign_swap hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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)
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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 ((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
have 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₁))
Tactic: convert! add_neg_cancel (G := N₁ ⊗[R'] N₂) _ using 6
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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₁))
⊢ 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
have 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₂))
Tactic: convert! add_neg_cancel (G := N₁ ⊗[R'] N₂) _ using 6
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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)
⊢ 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₁))
have 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))
Tactic: ext k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
⊢ 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))
have h : v ((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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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)
⊢ 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₂))
have 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))
Tactic: ext k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
⊢ 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))
have h : v ((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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
⊢ 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₂)
have 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₂)
Tactic: induction σ using Quotient.inductionOn' with | _ σ
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
σ : 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₂)
have h : HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' σ) = Quotient.mk'' σ →
  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: dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MultilinearMap.smul_apply,
    MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply, domCoprod.summand]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
σ : Perm (ιa ⊕ ιb)
hσ : HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' σ) = Quotient.mk'' σ
⊢ 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
have h : ∀ (sl : Perm ιa) (sr : Perm ιb)
  (hσ :
    (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
      ((fun (x : Perm (ιa ⊕ ιb)) ↦ swap i j • 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: obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
σ : Perm (ιa ⊕ ιb)
hσ_1 : HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' σ) = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦ swap i j • 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
have h : ∀ (i' : ιa) (hi : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) i : ιa ⊕ ιb) (Sum.inl i' : ιa ⊕ ιb)),
  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: rcases hi : σ⁻¹ i with i' | i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
σ : Perm (ιa ⊕ ιb)
hσ_1 : HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' σ) = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦ swap i j • x) σ)⁻¹ * σ
h :
  ∀ (i' : ιa) (hi : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) i : ιa ⊕ ιb) (Sum.inl i' : ιa ⊕ ιb)),
    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
⊢ 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
have h₁ : ∀ (i' : ιb) (hi : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) i : ιa ⊕ ιb) (Sum.inr i' : ιa ⊕ ιb)),
  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: rcases hi : σ⁻¹ i with i' | i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
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
σ : Perm (ιa ⊕ ιb)
hσ_1 : HSMul.hSMul (β := Perm.ModSumCongr ιa ιb) (swap i j) (Quotient.mk'' σ) = Quotient.mk'' σ
sl : Perm ιa
sr : Perm ιb
hσ :
  (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) =
    ((fun (x : Perm (ιa ⊕ ιb)) ↦ swap i j • x) σ)⁻¹ * σ
i' : ιa
hi : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) i : ιa ⊕ ιb) (Sum.inl i' : ιa ⊕ ιb)
⊢ 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
have h : ∀ (j' : ιa) (hj : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) j : ιa ⊕ ιb) (Sum.inl j' : ιa ⊕ ιb)),
  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: rcases hj : σ⁻¹ j with j' | j'