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 β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σ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 (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σ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)]
-- 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' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂ * σb')) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
have right₂ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σ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)]
-- 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' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb')
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂ * σb')) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
have right₃ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σ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)]
-- 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' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb')
right₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ 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₄ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σ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)]
-- 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' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb')
right₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ 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₅ : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inr b₁) (Sum.inr b₂)) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σ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)]
-- 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' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb')
right₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₅ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inr b₁) (Sum.inr b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ 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₆ : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inr b₁) (Sum.inr b₂)) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σ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)]
-- 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' : ℤˣ)
right :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        ((HMul.hMul (α := Perm α) 1 1).sumCongr (swap b₁ b₂ * σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₁ :
  Eq (α := ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ)
        (HMul.hMul (α := Perm (α ⊕ β)) (sumCongr 1 (swap b₁ b₂)) (sumCongr 1 σb')) :
      ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb') : ℤˣ)
right₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂ * σb')
right₃ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb') : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₄ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 (swap b₁ b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₅ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inr b₁) (Sum.inr b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (swap b₁ b₂) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ)
right₆ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (swap (Sum.inr b₁) (Sum.inr b₂)) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((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₇ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb' : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (-1 : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σ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)]
-- 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 (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have right : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
  (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) 1 : ℤˣ)
Tactic: induction σb using swap_induction_on with
    | one => simp
    | swap_mul σb' b₁ b₂ hb ih =>
      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)]
Cleared hypotheses: σb
-- 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 β
right :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 1) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) 1 : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have right₁ : ∀ (σ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') : ℤˣ)
Tactic: induction σb using swap_induction_on with
    | one => simp
    | swap_mul σb' b₁ b₂ hb ih =>
      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)]
Cleared hypotheses: σb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : ℤˣ
σ : Perm α
⊢ Membership.mem (γ := Finset (Perm α)) (ofSign s) σ ↔ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
have rw : Membership.mem (γ := Finset (Perm α)) {x : Perm α | ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) x = s} σ ↔
  ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
Tactic: rw [ofSign, mem_filter, and_iff_right (mem_univ σ)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : ℤˣ
σ : Perm α
rw :
  Membership.mem (γ := Finset (Perm α)) {x : Perm α | ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) x = s} σ ↔
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
⊢ Membership.mem (γ := Finset (Perm α)) (ofSign s) σ ↔ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
have rw₁ : Membership.mem (γ := Finset (Perm α)) univ σ ∧ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s ↔
  ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
Tactic: rw [ofSign, mem_filter, and_iff_right (mem_univ σ)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : ℤˣ
σ : Perm α
rw :
  Membership.mem (γ := Finset (Perm α)) {x : Perm α | ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) x = s} σ ↔
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
rw₁ :
  Membership.mem (γ := Finset (Perm α)) univ σ ∧ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s ↔
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
⊢ Membership.mem (γ := Finset (Perm α)) (ofSign s) σ ↔ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
have rw₂ : ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s ↔ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ = s
Tactic: rw [ofSign, mem_filter, and_iff_right (mem_univ σ)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
⊢ _root_.Disjoint.{u} (α := Finset (Perm α)) (ofSign 1) (ofSign (-1))
have rw : ∀ (a : Perm α),
  Membership.mem (γ := Finset (Perm α)) (ofSign 1) a →
    ∀ (b : Perm α), Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) b → a ≠ b
Tactic: rw [Finset.disjoint_iff_ne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ
hτ : Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ
⊢ False
have hσ₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)
Tactic: rw [mem_ofSign] at hσ hτ
Cleared hypotheses: hσ, hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ
hτ : Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ
hσ₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)
⊢ False
have hτ₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ)
Tactic: rw [mem_ofSign] at hσ hτ
Cleared hypotheses: hσ, hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
hσ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ)
hτ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ)
⊢ False
have this : Eq (α := ℤˣ) 1 (-1)
Tactic: have := hσ.symm.trans hτ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq.{u + 1} (α := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) ⋯) univ
have h : ∀ (σ : Perm α),
  Membership.mem (γ := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) sorry) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
Tactic: ext σ
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
⊢ Membership.mem (γ := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) ⋯) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
have h : Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ ∨ Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ ↔
  Membership.mem (γ := Finset (Perm α)) univ σ
Tactic: simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h :
  Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ ∨ Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
⊢ Membership.mem (γ := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) ⋯) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
have h₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ) ∨
    Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ) ↔
  Membership.mem (γ := Finset (Perm α)) univ σ
Tactic: simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h :
  Membership.mem (γ := Finset (Perm α)) (ofSign 1) σ ∨ Membership.mem (γ := Finset (Perm α)) (ofSign (-1)) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
h₁ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (1 : ℤˣ) ∨
      Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σ : ℤˣ) (-1 : ℤˣ) ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
⊢ Membership.mem (γ := Finset (Perm α)) (disjUnion (ofSign 1) (ofSign (-1)) ⋯) σ ↔
    Membership.mem (γ := Finset (Perm α)) univ σ
have h₂ : True ↔ Membership.mem (γ := Finset (Perm α)) univ σ
Tactic: simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
⊢ f.Disjoint f ↔ f = 1
have refine : ∀ (h : f.Disjoint f), f = 1
Tactic: refine ⟨fun h => ?_, fun h => h.symm ▸ disjoint_one_left 1⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
h : f.Disjoint f
⊢ f = 1
have H : ∀ (x : α), Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f : Perm α
h : f.Disjoint f
x : α
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
have H : ∀ (hx : (f : (a : α) → α) x = x), Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: rcases h x with hx | hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
⊢ (f⁻¹ : (a : α) → α) x = x ∨ (g : (a : α) → α) x = x
have rw : (f : (a : α) → α) x = x ∨ (g : (a : α) → α) x = x
Tactic: rw [inv_eq_iff_eq, eq_comm]