awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
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
⊢ 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 (hypothesis)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
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
have ha₃ : ¬a₁ = 1
Tactic: simp only [and_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂
Cleared hypotheses: ha₂
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 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)) 0 : Fin (n + 2)) then
      -1
    else 1)
    1
have this : 1 < a₁
Tactic: have : 1 < a₁ := lt_of_le_of_ne' (Nat.succ_le_of_lt ha₁) ha₂
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < 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
have h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0) 1
Tactic: have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1 := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0) 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)) 0 : Fin (n + 2)) then
      -1
    else 1)
    1
have inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 then -1 else 1) 1
Tactic: rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_ge]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0) 1
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 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)) 0 : Fin (n + 2)) then
      -1
    else 1)
    1
have inr₁ : Eq (α := ℤˣ) (if a₁ ≤ 1 then -1 else 1) 1
Tactic: rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_ge]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0) 1
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 0 then -1 else 1) 1
inr₁ : Eq (α := ℤˣ) (if a₁ ≤ 1 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)) 0 : Fin (n + 2)) then
      -1
    else 1)
    1
have inr₂ : Eq (α := ℤˣ) 1 1
Tactic: rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_ge]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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₁
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 le : 1 ≤ a₂
Tactic: have le : 1 ≤ a₂ := Nat.succ_le_of_lt H'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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₁
H' : 0 < a₂
le : 1 ≤ 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 lt : 1 < a₁
Tactic: have lt : 1 < a₁ := le.trans_lt ha₁
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < 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 h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
Tactic: have h01 : Equiv.swap (0 : Fin (n + 2)) 1 1 = 0 := by simp only [swap_apply_right]
-- 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₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : 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₁ : 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₁ 1 ∉
      {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
  (ha₁ : 1 < a₁) (H' : LT.lt (α := Fin (n + 2)) 0 1) (le : LE.le (α := Fin (n + 2)) 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)) 1 : Fin (n + 2)) then
      -1
    else 1)
    1
Tactic: rcases le.eq_or_lt with (rfl | lt')
Cleared hypotheses: a₂, ha₂, ha₁, H', le
-- 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₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
inr :
  ∀
    (ha₂ :
      Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 1 ∉
        {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0})
    (ha₁ : 1 < a₁) (H' : LT.lt (α := Fin (n + 2)) 0 1) (le : LE.le (α := Fin (n + 2)) 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)) 1 : 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₁ : ∀ (lt' : 1 < 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 le.eq_or_lt with (rfl | lt')
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 1 ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : 1 < a₁
H' : LT.lt (α := Fin (n + 2)) 0 1
le : LE.le (α := Fin (n + 2)) 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)) 1 : Fin (n + 2)) then
      -1
    else 1)
    1
have inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1 then -1 else 1) 1
Tactic: rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_ge]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 1 ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : 1 < a₁
H' : LT.lt (α := Fin (n + 2)) 0 1
le : LE.le (α := Fin (n + 2)) 1 1
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1 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)) 1 : Fin (n + 2)) then
      -1
    else 1)
    1
have inr₁ : Eq (α := ℤˣ) (if a₁ ≤ 0 then -1 else 1) 1
Tactic: rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_ge]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
ha₂ :
  Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) a₁ 1 ∉ {Sigma.mk (β := fun (x : Fin (n + 2)) ↦ Fin (n + 2)) 1 0}
ha₁ : 1 < a₁
H' : LT.lt (α := Fin (n + 2)) 0 1
le : LE.le (α := Fin (n + 2)) 1 1
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1 then -1 else 1) 1
inr₁ : Eq (α := ℤˣ) (if a₁ ≤ 0 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)) 1 : Fin (n + 2)) then
      -1
    else 1)
    1
have inr₂ : Eq (α := ℤˣ) 1 1
Tactic: rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_ge]
-- 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₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
lt' : 1 < 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 : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ then -1 else 1) 1
Tactic: rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
          swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_ge]
-- 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₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
lt' : 1 < a₂
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ 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₁ : Eq (α := ℤˣ) (if a₁ ≤ a₂ then -1 else 1) 1
Tactic: rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
          swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_ge]
-- 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₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : Eq (α := Fin (n + 2)) ((swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) 1) 0
lt' : 1 < a₂
inr : Eq (α := ℤˣ) (if a₁ ≤ (swap 0 1 : (a : Fin (n + 2)) → Fin (n + 2)) a₂ then -1 else 1) 1
inr₁ : Eq (α := ℤˣ) (if a₁ ≤ a₂ 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₂ : Eq (α := ℤˣ) 1 1
Tactic: rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
          swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_ge]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
hn : 2 ≤ n
⊢ (swap (⟨0, ⋯⟩ : Fin n) (⟨1, ⋯⟩ : Fin n)).signAux = -1
have zero : ∀ (hn : LE.le (α := ℕ) 2 0), (swap (⟨0, sorry⟩ : Fin 0) (⟨1, sorry⟩ : Fin 0)).signAux = -1
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
hn : 2 ≤ n
zero : ∀ (hn : LE.le (α := ℕ) 2 0), (swap (⟨0, ⋯⟩ : Fin 0) (⟨1, ⋯⟩ : Fin 0)).signAux = -1
⊢ (swap (⟨0, ⋯⟩ : Fin n) (⟨1, ⋯⟩ : Fin n)).signAux = -1
have succ : ∀ (hn : 2 ≤ HAdd.hAdd (α := ℕ) 0 1),
  (swap (⟨0, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) (⟨1, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))).signAux = -1
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
hn : 2 ≤ n
zero : ∀ (hn : LE.le (α := ℕ) 2 0), (swap (⟨0, ⋯⟩ : Fin 0) (⟨1, ⋯⟩ : Fin 0)).signAux = -1
succ :
  ∀ (hn : 2 ≤ HAdd.hAdd (α := ℕ) 0 1),
    (swap (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1))).signAux = -1
⊢ (swap (⟨0, ⋯⟩ : Fin n) (⟨1, ⋯⟩ : Fin n)).signAux = -1
have succ₁ : ∀ (n : ℕ) (hn : 2 ≤ n + 1 + 1), (swap (⟨0, sorry⟩ : Fin (n + 1 + 1)) (⟨1, sorry⟩ : Fin (n + 1 + 1))).signAux = -1
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ (swap x y).signAux = -1
have h2n : 2 ≤ n + 2
Tactic: have h2n : 2 ≤ n + 2 := by exact le_add_self
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ (swap x y).signAux = -1
have rw : IsConj (swap x y).signAux (swap (⟨0, sorry⟩ : Fin (n + 2)) (⟨1, sorry⟩ : Fin (n + 2))).signAux
Tactic: rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have this : f = 1
Tactic: have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) List.not_mem_nil)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
Tactic: rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have rw₁ : signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
Tactic: rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
rw₁ : signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have rw₂ : signAux (e.symm.trans e) = signAux2 [] (Equiv.refl α)
Tactic: rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
rw₁ : signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
rw₂ : signAux (e.symm.trans e) = signAux2 [] (Equiv.refl α)
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have rw₃ : signAux (n := n) (Equiv.refl (Fin n)) = signAux2 [] (Equiv.refl α)
Tactic: rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
rw₁ : signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
rw₂ : signAux (e.symm.trans e) = signAux2 [] (Equiv.refl α)
rw₃ : signAux (n := n) (Equiv.refl (Fin n)) = signAux2 [] (Equiv.refl α)
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have rw₄ : signAux (n := n) 1 = signAux2 [] (Equiv.refl α)
Tactic: rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
rw₁ : signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
rw₂ : signAux (e.symm.trans e) = signAux2 [] (Equiv.refl α)
rw₃ : signAux (n := n) (Equiv.refl (Fin n)) = signAux2 [] (Equiv.refl α)
rw₄ : signAux (n := n) 1 = signAux2 [] (Equiv.refl α)
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have rw₅ : 1 = signAux2 [] (Equiv.refl α)
Tactic: rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x
this : f = 1
rw : signAux (Equiv.trans (e.symm.trans 1) e) = signAux2.{u} (α := α) [] 1
rw₁ : signAux ((e.symm.trans (Equiv.refl α)).trans e) = signAux2 [] (Equiv.refl α)
rw₂ : signAux (e.symm.trans e) = signAux2 [] (Equiv.refl α)
rw₃ : signAux (n := n) (Equiv.refl (Fin n)) = signAux2 [] (Equiv.refl α)
rw₄ : signAux (n := n) 1 = signAux2 [] (Equiv.refl α)
rw₅ : 1 = signAux2 [] (Equiv.refl α)
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
have rw₆ : Eq (α := ℤˣ) 1 1
Tactic: rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
⊢ signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
have pos : ∀ (hfx : x = (f : (a : α) → α) x),
  signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
Tactic: by_cases hfx : x = f x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
pos :
  ∀ (hfx : x = (f : (a : α) → α) x),
    signAux ((e.symm.trans f).trans e) =
      if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
⊢ signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
have neg : ∀ (hfx : ¬x = (f : (a : α) → α) x),
  signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
Tactic: by_cases hfx : x = f x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = (f : (a : α) → α) x
⊢ signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
have pos : signAux ((e.symm.trans f).trans e) = signAux2 l f
Tactic: rw [if_pos hfx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
⊢ signAux ((e.symm.trans f).trans e) =
    if x = (f : (a : α) → α) x then signAux2 l f else -signAux2 l (swap x ((f : (a : α) → α) x) * f)
have hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
Tactic: have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
        have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
        List.mem_of_ne_of_mem this.2 (h _ this.1)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), (f : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
⊢ (e.symm.trans (swap x ((f : (a : α) → α) x) * f)).trans e =
    HMul.hMul (α := Perm (Fin n))
      (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n))
      ((e.symm.trans f).trans e)
have H : ∀ (x_1 : Fin n),
  (↑(((e.symm.trans (swap x ((f : (a : α) → α) x) * f)).trans e : (a : Fin n) → Fin n) x_1) : ℕ) =
    (↑((HMul.hMul (α := Perm (Fin n))
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n))
              ((e.symm.trans f).trans e) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)
Tactic: ext