awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
⊢ (if x :
        LT.lt (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n) then
      Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
    else
      Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))) ∈
    finPairsLT n
have pos : ∀
  (h :
    LT.lt (α := Fin n)
      ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
        Fin n)
      ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
        Fin n)),
  Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
      ((f : (a : Fin n) → Fin n)
        (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
      ((f : (a : Fin n) → Fin n)
        (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) ∈
    finPairsLT n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ finPairsLT n
pos :
  ∀
    (h :
      LT.lt (α := Fin n)
        ((f : (a : Fin n) → Fin n)
            (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
          Fin n)
        ((f : (a : Fin n) → Fin n)
            (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
          Fin n)),
    Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) ∈
      finPairsLT n
⊢ (if x :
        LT.lt (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
            Fin n) then
      Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
    else
      Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))) ∈
    finPairsLT n
have neg : ∀
  (h :
    ¬LT.lt (α := Fin n)
        ((f : (a : Fin n) → Fin n)
            (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
          Fin n)
        ((f : (a : Fin n) → Fin n)
            (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)) :
          Fin n)),
  Membership.mem (α := (_ : Fin n) × Fin n) (finPairsLT n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n)
        ((f : (a : Fin n) → Fin n)
          (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)))
        ((f : (a : Fin n) → Fin n)
          (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))) :
      (_ : Fin n) × Fin n)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n) then
      -1
    else 1)
    (if
        LE.le (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n) then
      -1
    else 1)
have pos : ∀
  (h :
    LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) b : Fin n)
      ((Equiv.symm f : (a : Fin n) → Fin n) a : Fin n)),
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n) then
      -1
    else 1)
    (if
        LE.le (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n) then
      -1
    else 1)
Tactic: by_cases h : f.symm b < f.symm a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
x : (_ : Fin n) × Fin n
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
pos :
  ∀
    (h :
      LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) b : Fin n)
        ((Equiv.symm f : (a : Fin n) → Fin n) a : Fin n)),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin n)
            ((f⁻¹ : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
              Fin n)
            ((f⁻¹ : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
              Fin n) then
        -1
      else 1)
      (if
          LE.le (α := Fin n)
            ((f : (a : Fin n) → Fin n)
                ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n)
            ((f : (a : Fin n) → Fin n)
                ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
              Fin n) then
        -1
      else 1)
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n) then
      -1
    else 1)
    (if
        LE.le (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n) then
      -1
    else 1)
have neg : ∀
  (h :
    ¬LT.lt (α := Fin n) ((Equiv.symm f : (a : Fin n) → Fin n) b : Fin n)
        ((Equiv.symm f : (a : Fin n) → Fin n) a : Fin n)),
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n)
          ((f⁻¹ : (a : Fin n) → Fin n)
              (Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)) :
            Fin n) then
      -1
    else 1)
    (if
        LE.le (α := Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).fst (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n)
          ((f : (a : Fin n) → Fin n)
              ((f⁻¹.signBijAux (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)).snd (β := fun (x : Fin n) ↦ Fin n)) :
            Fin n) then
      -1
    else 1)
Tactic: by_cases h : f.symm b < f.symm a
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f g : Perm (Fin n)
⊢ (f * g).signAux = f.signAux * g.signAux
have rw : (f * g).signAux = f.signAux * g⁻¹.signAux
Tactic: rw [← signAux_inv g]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f * g : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1) =
    HMul.hMul (α := ℤˣ)
      (∏ x ∈ finPairsLT n,
        if
            LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((f : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
      (∏ x ∈ finPairsLT n,
        if
            LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
have rw : Eq (α := ℤˣ)
  (∏ x ∈ finPairsLT n,
    if
        LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
          ((f * g : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
      -1
    else 1)
  (∏ x ∈ finPairsLT n,
    HMul.hMul (α := ℤˣ)
      (if
          LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
      (if
          LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((g⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1))
Tactic: rw [← prod_mul_distrib]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f g : Perm (Fin n)
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f * g : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ x ∈ finPairsLT n,
      HMul.hMul (α := ℤˣ)
        (if
            LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((f : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1)
        (if
            LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
              ((g⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
          -1
        else 1))
have refine : ∀ a ∈ finPairsLT n,
  (if
        LE.le (α := Fin n) ((f * g : (a : Fin n) → Fin n) (a.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
          ((f * g : (a : Fin n) → Fin n) (a.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
      -1
    else 1) =
    HMul.hMul (α := ℤˣ)
      (if
          LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) ((g.signBijAux a).fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((f : (a : Fin n) → Fin n) ((g.signBijAux a).snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
      (if
          LE.le (α := Fin n) ((g⁻¹ : (a : Fin n) → Fin n) ((g.signBijAux a).fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((g⁻¹ : (a : Fin n) → Fin n) ((g.signBijAux a).snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
Tactic: refine prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b ∈ finPairsLT n
⊢ (if
        LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) ((g : (a : Fin n) → Fin n) a) : Fin n)
          ((f : (a : Fin n) → Fin n) ((g : (a : Fin n) → Fin n) b) : Fin n) then
      -1
    else 1) =
    HMul.hMul (α := ℤˣ)
      (if
          LE.le (α := Fin n)
            ((f : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n)
            ((f : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n) then
        -1
      else 1)
      (if
          LE.le (α := Fin n)
            ((g⁻¹ : (a : Fin n) → Fin n)
                (Sigma.fst (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n)
            ((g⁻¹ : (a : Fin n) → Fin n)
                (Sigma.snd (β := fun (x : Fin n) ↦ Fin n)
                  (if x :
                      LT.lt (α := Fin n) ((g : (a : Fin n) → Fin n) b : Fin n)
                        ((g : (a : Fin n) → Fin n) a : Fin n) then
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) a) ((g : (a : Fin n) → Fin n) b)
                  else
                    Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((g : (a : Fin n) → Fin n) b)
                      ((g : (a : Fin n) → Fin n) a))) :
              Fin n) then
        -1
      else 1)
have hab₁ : Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b) <
  Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a b)
Tactic: rw [mem_finPairsLT] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
⊢ signAux (n := n + 2) (swap 0 1) =
    ∏ x ∈ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0},
      if
          LE.le (α := Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (x.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
              Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (x.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
              Fin (n + 2)) then
        -1
      else 1
have refine : ∀ (a : (_ : Fin (n + 2)) × Fin (n + 2))
  (ha₁ : Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2)) a)
  (ha₂ : a ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}),
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
            Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
            Fin (n + 2)) then
      -1
    else 1)
    1
Tactic: refine Eq.symm (prod_subset (fun ⟨x₁, x₂⟩ => by
      simp +contextual [mem_finPairsLT]) fun a ha₁ ha₂ => ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2)) a
ha₂ : a ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
            Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) (a.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))) :
            Fin (n + 2)) then
      -1
    else 1)
    1
have rcases : ∀ (a₁ a₂ : Fin (n + 2))
  (ha₁ :
    Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2))
      (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂))
  (ha₂ :
    Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉
      {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}),
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2)) then
      -1
    else 1)
    1
Tactic: rcases a with ⟨a₁, a₂⟩
Cleared hypotheses: a, ha₁, ha₂
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₁ :
  Membership.mem (γ := Finset ((_ : Fin (n + 2)) × Fin (n + 2))) (finPairsLT (n + 2))
    (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2)) then
      -1
    else 1)
    1
have ha₃ : a₂ < a₁
Tactic: replace ha₁ : a₂ < a₁ := mem_finPairsLT.1 ha₁
Cleared hypotheses: ha₁
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.fst (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2))
              (Sigma.snd (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2))
                (Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂)) :
            Fin (n + 2)) then
      -1
    else 1)
    1
have dsimp : Eq (α := ℤˣ)
  (if
      LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
        ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
    -1
  else 1)
  1
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1
have inl : ∀
  (ha₂ :
    Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 0 a₂ ∉
      {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
  (ha₁ : a₂ < 0),
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1
Tactic: rcases a₁.zero_le.eq_or_lt with (rfl | H)
Cleared hypotheses: a₁, ha₂, ha₁
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
inl :
  ∀
    (ha₂ :
      Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 0 a₂ ∉
        {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
    (ha₁ : a₂ < 0),
    Eq (α := ℤˣ)
      (if
          LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2))
            ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
        -1
      else 1)
      1
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1
have inr : ∀ (H : 0 < a₁),
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1
Tactic: rcases a₁.zero_le.eq_or_lt with (rfl | H)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ a₂ ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : a₂ < a₁
H : 0 < a₁
⊢ Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ : Fin (n + 2)) then
      -1
    else 1)
    1
have inr : ∀
  (ha₂ :
    Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 0 ∉
      {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
  (ha₁ : 0 < a₁),
  Eq (α := ℤˣ)
    (if
        LE.le (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₁ : Fin (n + 2))
          ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 : Fin (n + 2)) then
      -1
    else 1)
    1
Tactic: rcases a₂.zero_le.eq_or_lt with (rfl | H')
Cleared hypotheses: a₂, ha₂, ha₁