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
σ : 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)
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
⊢ 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' : ιb) (hj : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) j : ιa ⊕ ιb) (Sum.inr 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'
-- 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' : ι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
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'
-- 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' : ιb
hi : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) i : ιa ⊕ ιb) (Sum.inr i' : ιa ⊕ ιb)
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
⊢ 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' : ιb) (hj : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) j : ιa ⊕ ιb) (Sum.inr 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'
-- 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)
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
have h : ∀ (hi : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) (j' : ιa) (hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')),
  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: rw [Perm.inv_eq_iff_eq] at hi hj
Cleared hypotheses: hi, j', hj
-- 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)
j' : ιb
hj : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) j : ιa ⊕ ιb) (Sum.inr 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
have h : ∀ (hi : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) (j' : ιb) (hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')),
  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: rw [Perm.inv_eq_iff_eq] at hi hj
Cleared hypotheses: hi, j', hj
-- 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' : ιb
hi : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) i : ιa ⊕ ιb) (Sum.inr i' : ιa ⊕ ιb)
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
have h : ∀ (hi : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) (j' : ιa) (hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')),
  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: rw [Perm.inv_eq_iff_eq] at hi hj
Cleared hypotheses: hi, j', hj
-- 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' : ιb
hi : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) i : ιa ⊕ ιb) (Sum.inr i' : ιa ⊕ ιb)
j' : ιb
hj : Eq (α := ιa ⊕ ιb) ((σ⁻¹ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) j : ιa ⊕ ιb) (Sum.inr 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
have h : ∀ (hi : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr i')) (j' : ιb) (hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inr j')),
  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: rw [Perm.inv_eq_iff_eq] at hi hj
Cleared hypotheses: hi, j', hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (hypothesis)
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 : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')
j' : ιa
hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')
⊢ 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 hv₁ : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
Tactic: substs hi hj
Cleared hypotheses: i, j, hv, hij, hσ_1, hσ, hi, hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (hypothesis)
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 : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')
j' : ιa
hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')
hv₁ : v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')) = v ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j'))
⊢ 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 hij₁ : Ne (α := ιa ⊕ ιb) ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i') : ιa ⊕ ιb)
  ((σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j') : ιa ⊕ ιb)
Tactic: substs hi hj
Cleared hypotheses: i, j, hv, hij, hσ_1, hσ, hi, hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (hypothesis)
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 : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')
j' : ιa
hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')
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)
⊢ 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σ₁ : 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'' σ
Tactic: substs hi hj
Cleared hypotheses: i, j, hv, hij, hσ_1, hσ, hi, hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (hypothesis)
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 : i = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl i')
j' : ιa
hj : j = (σ : (a : ιa ⊕ ιb) → ιa ⊕ ιb) (Sum.inl j')
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σ₁ :
  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'' σ
⊢ 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σ₂ : (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)
        σ)⁻¹ *
    σ
Tactic: substs hi hj
Cleared hypotheses: i, j, hv, hij, hσ_1, hσ, hi, hj