awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
x : Fin n
⊢ (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
have H : ∀ (ch : x < i), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_trichotomy x i with ch | ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
x : Fin n
H : ∀ (ch : x < i), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
have H₁ : ∀ (ch : x = i), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_trichotomy x i with ch | ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
x : Fin n
H : ∀ (ch : x < i), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
H₁ : ∀ (ch : x = i), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
have H₂ : ∀ (ch : i < x), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_trichotomy x i with ch | ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
⊢ Eq (α := Fin n → Fin n)
    (Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n))
    (⇑(i.cycleIcc k) : (a : Fin n) → Fin n)
have h : ∀ (x : Fin n),
  (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h : ∀ (ch : x < i),
  (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_or_ge x i with ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
h :
  ∀ (ch : x < i),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h₁ : ∀ (ch : i ≤ x),
  (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_or_ge x i with ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h : ∀ (ch : k < x),
  (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_or_ge k x with ch | ch1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
h :
  ∀ (ch : k < x),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h₁ : ∀ (ch1 : x ≤ k),
  (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_or_ge k x with ch | ch1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h : ∀ (ch2 : x < j),
  (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_or_ge x j with ch2 | ch2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
h :
  ∀ (ch2 : x < j),
    (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
        ℕ) =
      (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h₁ : ∀ (ch2 : j ≤ x),
  (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
Tactic: rcases lt_or_ge x j with ch2 | ch2
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h : (↑(if x = j then i else x + 1) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
Tactic: simp [cycleIcc_of_lt ch2, cycleIcc_of_le_of_le ch ch1, cycleIcc_of_le_of_le ch (le_of_lt ch2)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
⊢ (↑(if x = j then i else x + 1) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
have pos : x = j → x = k → (↑i : ℕ) = (↑i : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
pos : x = j → x = k → (↑i : ℕ) = (↑i : ℕ)
⊢ (↑(if x = j then i else x + 1) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
have neg : x = j → ¬x = k → (↑i : ℕ) = (↑(x + 1) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
pos : x = j → x = k → (↑i : ℕ) = (↑i : ℕ)
neg : x = j → ¬x = k → (↑i : ℕ) = (↑(x + 1) : ℕ)
⊢ (↑(if x = j then i else x + 1) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
have pos₁ : ¬x = j → x = k → (↑(x + 1) : ℕ) = (↑i : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : x < j
pos : x = j → x = k → (↑i : ℕ) = (↑i : ℕ)
neg : x = j → ¬x = k → (↑i : ℕ) = (↑(x + 1) : ℕ)
pos₁ : ¬x = j → x = k → (↑(x + 1) : ℕ) = (↑i : ℕ)
⊢ (↑(if x = j then i else x + 1) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
have neg₁ : ¬x = j → ¬x = k → (↑(x + 1) : ℕ) = (↑(x + 1) : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
⊢ (↑(Function.comp (β := Fin n) (⇑(i.cycleIcc j) : (a : Fin n) → Fin n) (⇑(j.cycleIcc k) : (a : Fin n) → Fin n) x) :
      ℕ) =
    (↑((i.cycleIcc k : (a : Fin n) → Fin n) x) : ℕ)
have h : (↑((i.cycleIcc j : (a : Fin n) → Fin n) (if x = k then j else x + 1)) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
Tactic: simp only [Function.comp_apply, cycleIcc_of_le_of_le ch2 ch1, cycleIcc_of_le_of_le ch ch1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
⊢ (↑((i.cycleIcc j : (a : Fin n) → Fin n) (if x = k then j else x + 1)) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
have pos : ∀ (h : x = k), (↑((i.cycleIcc j : (a : Fin n) → Fin n) j) : ℕ) = (↑i : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
inst : NeZero n
hij : i ≤ j
hjk : j ≤ k
x : Fin n
ch : i ≤ x
ch1 : x ≤ k
ch2 : j ≤ x
pos : ∀ (h : x = k), (↑((i.cycleIcc j : (a : Fin n) → Fin n) j) : ℕ) = (↑i : ℕ)
⊢ (↑((i.cycleIcc j : (a : Fin n) → Fin n) (if x = k then j else x + 1)) : ℕ) = (↑(if x = k then i else x + 1) : ℕ)
have neg : ∀ (h : ¬x = k), (↑((i.cycleIcc j : (a : Fin n) → Fin n) (x + 1)) : ℕ) = (↑(x + 1) : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
h : (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
⊢ Eq (α := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
    (∏ j : Fin n,
        ∏ i ∈ Finset.Iio j,
          if LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n) then 1
          else -1 :
      ℤˣ)
have rw : Eq (α := ℤˣ)
  (∏ x ∈ finPairsLT n,
    if
        LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
          ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
      -1
    else 1)
  (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
    if
        LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
          ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
      1
    else -1)
Tactic: rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
h : (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
      if
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
            ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
        1
      else -1)
have h₁ : Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio = finPairsLT n
Tactic: convert! rfl using 2 with x hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
h : (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
h₁ : Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio = finPairsLT n
⊢ Eq (α := ℤˣ)
    (∏ x ∈ finPairsLT n,
      if
          LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
        -1
      else 1)
    (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
      if
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
            ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
        1
      else -1)
have h₂ : ∀ (x : (_ : Fin n) × Fin n) (hx : x ∈ finPairsLT n),
  Eq (α := ℤˣ)
    (if
        LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
          ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
      1
    else -1)
    (if
        LE.le (α := Fin n) ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (x : Fin n) ↦ Fin n)) : Fin n)
          ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (x : Fin n) ↦ Fin n)) : Fin n) then
      -1
    else 1)
Tactic: convert! rfl using 2 with x hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
    (∏ j : Fin n,
        ∏ i ∈ Finset.Iio j,
          if LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n) then 1
          else -1 :
      ℤˣ)
have suffices : (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
Tactic: suffices h : σ.sign = σ.signAux by
    rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
    convert! rfl using 2 with x hx
    · simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]
    simp [← ite_not (p := _ ≤ _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
have refine : ∀ (π : Perm (Fin n)) (i j : Fin n) (hne : i ≠ j) (h_eq : (sign : (a : Perm (Fin n)) → ℤˣ) π = π.signAux),
  (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j * π).signAux
Tactic: refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : (sign : (a : Perm (Fin n)) → ℤˣ) π = π.signAux
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j * π).signAux
have rw : (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j).signAux * π.signAux
Tactic: rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : (sign : (a : Perm (Fin n)) → ℤˣ) π = π.signAux
rw : (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j).signAux * π.signAux
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j * π).signAux
have rw₁ : HMul.hMul (α := ℤˣ) (β := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) (swap i j) : ℤˣ)
    ((sign : (a : Perm (Fin n)) → ℤˣ) π : ℤˣ) =
  (swap i j).signAux * π.signAux
Tactic: rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : (sign : (a : Perm (Fin n)) → ℤˣ) π = π.signAux
rw : (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j).signAux * π.signAux
rw₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) (swap i j) : ℤˣ)
      ((sign : (a : Perm (Fin n)) → ℤˣ) π : ℤˣ) =
    (swap i j).signAux * π.signAux
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j * π).signAux
have rw₂ : HMul.hMul (α := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) (swap i j) : ℤˣ) π.signAux = (swap i j).signAux * π.signAux
Tactic: rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : (sign : (a : Perm (Fin n)) → ℤˣ) π = π.signAux
rw : (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j).signAux * π.signAux
rw₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) (swap i j) : ℤˣ)
      ((sign : (a : Perm (Fin n)) → ℤˣ) π : ℤˣ) =
    (swap i j).signAux * π.signAux
rw₂ : HMul.hMul (α := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) (swap i j) : ℤˣ) π.signAux = (swap i j).signAux * π.signAux
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j * π).signAux
have rw₃ : -1 * π.signAux = (swap i j).signAux * π.signAux
Tactic: rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : (sign : (a : Perm (Fin n)) → ℤˣ) π = π.signAux
rw : (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j).signAux * π.signAux
rw₁ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) (swap i j) : ℤˣ)
      ((sign : (a : Perm (Fin n)) → ℤˣ) π : ℤˣ) =
    (swap i j).signAux * π.signAux
rw₂ : HMul.hMul (α := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) (swap i j) : ℤˣ) π.signAux = (swap i j).signAux * π.signAux
rw₃ : -1 * π.signAux = (swap i j).signAux * π.signAux
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j * π).signAux
have rw₄ : -1 * π.signAux = -1 * π.signAux
Tactic: rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) σ : ℤˣ)
    (∏ i : Fin n,
        ∏ j ∈ Finset.Ioi i,
          if LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n) then 1
          else -1 :
      ℤˣ)
have rw : Eq (α := ℤˣ)
  (∏ j : Fin n,
    ∏ i ∈ Finset.Iio j,
      if LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n) then 1 else -1)
  (∏ i : Fin n,
    ∏ j ∈ Finset.Ioi i,
      if LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n) then 1 else -1)
Tactic: rw [σ.sign_eq_prod_prod_Iio]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ j : Fin n, ∏ i ∈ Finset.Iio j, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j)
have simp_rw : Eq.{u_1 + 1} (α := R)
  (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
    f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
      ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
  (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
    (↑(↑(if
                  LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                    ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                1
              else -1) :
            ℤ) :
        R) *
      f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
Tactic: simp_rw [← σ.sign_inv, σ⁻¹.sign_eq_prod_prod_Iio, Finset.prod_sigma', Units.coe_prod,
    Int.cast_prod, ← Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ Eq.{u_1 + 1} (α := R)
    (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏ x ∈ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio,
      (↑(↑(if
                    LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
have set : let D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio;
∀ (hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio),
  Eq.{u_1 + 1} (α := R)
    (∏ x ∈ D,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏ x ∈ D,
      (↑(↑(if
                    LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
Tactic: set D := (Finset.univ : Finset (Fin n)).sigma Finset.Iio with hD
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
⊢ Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
have h : ∀ (x1 x2 : Fin n),
  Membership.mem (γ := Finset ((_ : Fin n) × Fin n))
      (Finset.image
        (fun (x : (_ : Fin n) × Fin n) ↦
          Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
            (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
            (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
        D)
      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x1 x2) ↔
    Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x1 x2 ∈ D
Tactic: ext ⟨x1, x2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
x1 x2 : Fin n
⊢ Membership.mem (γ := Finset ((_ : Fin n) × Fin n))
      (Finset.image
        (fun (x : (_ : Fin n) × Fin n) ↦
          Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
            (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
            (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
        D)
      (Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x1 x2) ↔
    Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x1 x2 ∈ D
have h : (∃ (a : Fin n),
    ∃ b < a,
      max ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x1 ∧
        min ((σ : (a : Fin n) → Fin n) a) ((σ : (a : Fin n) → Fin n) b) = x2) ↔
  x2 < x1
Tactic: suffices (∃ a, ∃ b < a, σ a ⊔ σ b = x1 ∧ σ a ⊓ σ b = x2) ↔ x2 < x1 by simpa [hD]