awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
this :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw₁ :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
rw₂ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1 * sumCongr 1 σb) : ℤˣ)
rw₃ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((σa * 1).sumCongr (1 * σb)) : ℤˣ)
rw₄ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((σa * 1).sumCongr σb) : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have rw₅ : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
  (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
Tactic: rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have suffices : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
Tactic: suffices sign (sumCongr σa (1 : Perm β)) = sign σa ∧ sign (sumCongr (1 : Perm α) σb) = sign σb
    by rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have left : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
left :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have right : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
  (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left : Eq (α := ℤˣ)
  (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
    ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left₁ : Eq (α := ℤˣ)
  (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
      (HMul.hMul (α := Perm (α ⊕ β)) ((swap a₁ a₂).sumCongr 1) (σa'.sumCongr 1)) :
    ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) ((swap a₁ a₂).sumCongr 1) (σa'.sumCongr 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left₂ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
  ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa')
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) ((swap a₁ a₂).sumCongr 1) (σa'.sumCongr 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa')
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left₃ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) ((swap a₁ a₂).sumCongr 1) (σa'.sumCongr 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa')
left₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left₄ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) ((swap a₁ a₂).sumCongr 1) (σa'.sumCongr 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa')
left₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left₅ : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inl a₁) (Sum.inl a₂)) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) ((swap a₁ a₂).sumCongr 1) (σa'.sumCongr 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa')
left₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left₅ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inl a₁) (Sum.inl a₂)) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left₆ : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inl a₁) (Sum.inl a₂)) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((swap a₁ a₂ * σa').sumCongr (HMul.hMul (α := Perm β) 1 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) ((swap a₁ a₂).sumCongr 1) (σa'.sumCongr 1)) :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
left₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa')
left₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂).sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left₅ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inl a₁) (Sum.inl a₂)) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
left₆ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inl a₁) (Sum.inl a₂)) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
have left₇ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)
Tactic: rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
have left : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 : ℤˣ)
Tactic: induction σa using swap_induction_on with
    | one => simp
    | swap_mul σa' a₁ a₂ ha ih =>
      rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
Cleared hypotheses: σa
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
left :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
have left₁ : ∀ (σa' : Perm α) (a₁ a₂ : α) (ha : a₁ ≠ a₂)
  (ih :
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa'.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa' : ℤˣ)),
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((swap a₁ a₂ * σa').sumCongr 1) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap a₁ a₂ * σa') : ℤˣ)
Tactic: induction σa using swap_induction_on with
    | one => simp
    | swap_mul σa' a₁ a₂ ha ih =>
      rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
Cleared hypotheses: σa
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂ * σb')) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
have right : Eq (α := ℤˣ)
  (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
    ℤˣ)
  (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
Tactic: rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap,
        sign_swap hb, sign_swap (Sum.inr_injective.ne_iff.mpr hb)]