awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₃ : swap w y * (swap x z * swap w x) * (swap x z * swap w y) = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
rw₃ : swap w y * (swap x z * swap w x) * (swap x z * swap w y) = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₄ : swap w y * (swap x z * swap w x * (swap x z * swap w y)) = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
rw₃ : swap w y * (swap x z * swap w x) * (swap x z * swap w y) = swap y z
rw₄ : swap w y * (swap x z * swap w x * (swap x z * swap w y)) = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₅ : swap w y * (swap x z * swap w x * swap x z * swap w y) = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
rw₃ : swap w y * (swap x z * swap w x) * (swap x z * swap w y) = swap y z
rw₄ : swap w y * (swap x z * swap w x * (swap x z * swap w y)) = swap y z
rw₅ : swap w y * (swap x z * swap w x * swap x z * swap w y) = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₆ : swap w y * (swap z w * swap w y) = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
rw₃ : swap w y * (swap x z * swap w x) * (swap x z * swap w y) = swap y z
rw₄ : swap w y * (swap x z * swap w x * (swap x z * swap w y)) = swap y z
rw₅ : swap w y * (swap x z * swap w x * swap x z * swap w y) = swap y z
rw₆ : swap w y * (swap z w * swap w y) = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₇ : swap w y * swap z w * swap w y = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y_1 z_1 : α
hwx : w ≠ x
hyz_1 : y_1 ≠ z_1
y z : α
hyz : y ≠ z
hwz : w ≠ z
rw : swap w y * swap x z * swap w x * ((swap x z)⁻¹ * (swap w y)⁻¹) = swap y z
rw₁ : swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
rw₂ : swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
rw₃ : swap w y * (swap x z * swap w x) * (swap x z * swap w y) = swap y z
rw₄ : swap w y * (swap x z * swap w x * (swap x z * swap w y)) = swap y z
rw₅ : swap w y * (swap x z * swap w x * swap x z * swap w y) = swap y z
rw₆ : swap w y * (swap z w * swap w y) = swap y z
rw₇ : swap w y * swap z w * swap w y = swap y z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
have rw₈ : swap y z = swap y z
Tactic: rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ w ≠ y
have rw : z ≠ y
Tactic: rw [hwz]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
hwy : w ≠ y
⊢ swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z
have rw : swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap z y
Tactic: rw [swap_comm y z, h hyz.symm hwy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
hwy : w ≠ y
rw : swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap z y
⊢ swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z
have rw₁ : swap z y = swap z y
Tactic: rw [swap_comm y z, h hyz.symm hwy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
| Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    1
have rhs : 1
Tactic: rhs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
| 1
have rw : ∏ _x ∈ finPairsLT n, 1
Tactic: rw [← @Finset.prod_const_one _ _ (finPairsLT n)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
| Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    1
have rw : ∏ _x ∈ finPairsLT n, 1
Tactic: rhs; rw [← @Finset.prod_const_one _ _ (finPairsLT n)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    1
have conv : Eq (α := ℤˣ)
  (∏ x ∈ finPairsLT n,
    if
        LE.le (α := Fin n) ((1 : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
          ((1 : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
      -1
    else 1)
  (∏ _x ∈ finPairsLT n, 1)
Tactic: conv => rhs; rw [← @Finset.prod_const_one _ _ (finPairsLT n)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂ ∈ (↑(finPairsLT n) : Set ((_ : Fin n) × Fin n))
b₁ b₂ : Fin n
hb : Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂ ∈ (↑(finPairsLT n) : Set ((_ : Fin n) × Fin n))
h :
  Eq (α := (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
have rw : ∀
  (ha :
    Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
      Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂))
  (b₁ b₂ : Fin n)
  (hb :
    Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
      Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂))
  (h :
    Eq (α := (_ : Fin n) × Fin n)
      (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
          Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
        else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
        (_ : Fin n) × Fin n)
      (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
          Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
        else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
        (_ : Fin n) × Fin n)),
  Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
Tactic: rw [Finset.mem_coe, mem_finPairsLT] at *
Cleared hypotheses: ha, b₁, b₂, hb, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
have this : ¬b₁ < b₂
Tactic: have : ¬b₁ < b₂ := hb.le.not_gt
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
this : ¬b₁ < b₂
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
have pos : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) →
  LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
    ∀
      (h :
        Eq (α := (_ : Fin n) × Fin n)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
            (_ : Fin n) × Fin n)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂) :
            (_ : Fin n) × Fin n)),
      Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
        (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (if LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) then
        Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂)
      else Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
this : ¬b₁ < b₂
pos :
  LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) →
    LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
      ∀
        (h :
          Eq (α := (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
              (_ : Fin n) × Fin n)
            (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂) :
              (_ : Fin n) × Fin n)),
        Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
have neg : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n) →
  ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
    ∀
      (h :
        Eq (α := (_ : Fin n) × Fin n)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
            (_ : Fin n) × Fin n)
          (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
            (_ : Fin n) × Fin n)),
      Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
        (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
Tactic: split_ifs at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
this : ¬b₁ < b₂
h_1 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n)
h_2 : ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₁) ((f : (a : Fin n) → Fin n) a₂) :
      (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₂) ((f : (a : Fin n) → Fin n) b₁) :
      (_ : Fin n) × Fin n)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
have neg : ∀ (ha : b₁ < b₂) (hb : b₂ < b₁) (this : b₂ ≤ b₁),
  LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) →
    LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) →
      ∀ (h : a₁ = b₂ ∧ a₂ = b₁), b₂ = b₁ ∧ b₁ = b₂
Tactic: simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]
Cleared hypotheses: ha, hb, this, h_1, h_2, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
b₁ b₂ : Fin n
hb :
  Sigma.snd (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂) <
    Sigma.fst (β := fun (x : Fin n) ↦ Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
this : ¬b₁ < b₂
h_1 : ¬LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) a₂ : Fin n) ((f : (a : Fin n) → Fin n) a₁ : Fin n)
h_2 : LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n)
h :
  Eq (α := (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) a₂) ((f : (a : Fin n) → Fin n) a₁) :
      (_ : Fin n) × Fin n)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) ((f : (a : Fin n) → Fin n) b₁) ((f : (a : Fin n) → Fin n) b₂) :
      (_ : Fin n) × Fin n)
⊢ Eq (α := (_ : Fin n) × Fin n) (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) a₁ a₂)
    (Sigma.mk (β := fun (x : Fin n) ↦ Fin n) b₁ b₂)
have pos : ∀ (ha : b₁ < b₂) (hb : b₂ < b₁) (this : b₂ ≤ b₁),
  LE.le (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
    LT.lt (α := Fin n) ((f : (a : Fin n) → Fin n) b₂ : Fin n) ((f : (a : Fin n) → Fin n) b₁ : Fin n) →
      ∀ (h : a₂ = b₁ ∧ a₁ = b₂), b₂ = b₁ ∧ b₁ = b₂
Tactic: simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]
Cleared hypotheses: ha, hb, this, h_1, h_2, h