awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Fin
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 ∈ 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)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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)
⊢ 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:
convert! rfl using 2 with x hx

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
h : (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
⊢ Finset.sigma (α := fun (a : Fin n) ↦ Fin n) Finset.univ Finset.Iio = finPairsLT n

Tactic:
simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]

Premises used: Finset.ext_iff, Equiv.Perm.mem_finPairsLT
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
h : (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux
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:
simp [← ite_not (p := _ ≤ _)]

Premises used: LE.le, ite_not
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
suffices : (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 :
      ℤˣ)

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 := _ ≤ _)]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) 1 = signAux (n := n) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
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
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) σ = σ.signAux

Tactic:
refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
-- Module: Mathlib.GroupTheory.Perm.Fin
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
rw₄ rw₅ : -1 * π.signAux = -1 * π.signAux
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (swap i j * π) = (swap i j * π).signAux

Tactic:
rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]

Premises used: Equiv.Perm.signAux_swap, Equiv.Perm.sign_mul, Equiv.Perm.sign_swap, Equiv.Perm.signAux_mul
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
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)
⊢ 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 :
      ℤˣ)

Tactic:
rw [σ.sign_eq_prod_prod_Iio]

Premises used: Equiv.Perm.sign_eq_prod_prod_Iio
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (x y : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ x ∧ y ∈ Finset.Iio x ↔
      x ∈ Finset.Ioi y ∧ Membership.mem (γ := Finset (Fin n)) Finset.univ y

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
σ : Perm (Fin n)
⊢ 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:
apply Finset.prod_comm' (by simp)

Premises used: Finset.prod_comm'
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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)))
⊢ ∏ 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)

Tactic:
simp_rw [← σ.sign_inv, σ⁻¹.sign_eq_prod_prod_Iio, Finset.prod_sigma', Units.coe_prod,
    Int.cast_prod, ← Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, Units.coe_prod, Equiv.Perm.sign_eq_prod_prod_Iio, Inv.inv, Finset.prod_sigma', Equiv.Perm.sign_inv, Int.cast_prod
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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)))
⊢ 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:
set D := (Finset.univ : Finset (Fin n)).sigma Finset.Iio with hD

Premises used: Finset.univ, Finset.Iio, Finset.sigma
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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
⊢ 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

Tactic:
ext ⟨x1, x2⟩
-- Module: Mathlib.GroupTheory.Perm.Fin
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
this :
  (∃ (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
⊢ 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:
simpa [hD]
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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
⊢ 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:
suffices (∃ a, ∃ b < a, σ a ⊔ σ b = x1 ∧ σ a ⊓ σ b = x2) ↔ x2 < x1 by simpa [hD]
-- Module: Mathlib.GroupTheory.Perm.Fin
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
⊢ (∃ (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:
⟨?_, fun hlt ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.GroupTheory.Perm.Fin
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
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
h₁ :
  ∀ (hlt : x2 < x1),
    ∃ (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
⊢ (∃ (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:
refine ⟨?_, fun hlt ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Perm.Fin
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
i j : Fin n
hij : j < i
⊢ Ne (α := Fin n) (min ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) : Fin n)
    (max ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) : Fin n)

Tactic:
simp [hij.ne.symm]

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Fin
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
i j : Fin n
hij : j < i
⊢ LT.lt (α := Fin n) (min ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) : Fin n)
    (max ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) : Fin n)

Tactic:
exact inf_le_sup.lt_of_ne <| by simp [hij.ne.symm]

Premises used: inf_le_sup, LE.le.lt_of_ne
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hlt : x2 < x1
h :
  ∀
    (hlt' :
      LT.lt (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)
        ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n)),
    ∃ (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
h₁ :
  ∀
    (hle :
      LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n)
        ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)),
    ∃ (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
⊢ ∃ (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

Tactic:
obtain hlt' | hle := lt_or_ge (σ.symm x1) (σ.symm x2)

Premises used: lt_or_ge, Equiv.symm, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hlt : x2 < x1
hlt' :
  LT.lt (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n)
⊢ max ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2))
        ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1)) =
      x1 ∧
    min ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2))
        ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1)) =
      x2

Tactic:
simp [hlt.le]

Premises used: LT.lt.le
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hlt : x2 < x1
hlt' :
  LT.lt (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n)
⊢ ∃ (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

Tactic:
exact ⟨_, _, hlt', by simp [hlt.le]⟩
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hlt : x2 < x1
hle :
  LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)
⊢ Ne (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)

Tactic:
simp [hlt.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hlt : x2 < x1
hle :
  LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)
⊢ max ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1))
        ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2)) =
      x1 ∧
    min ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1))
        ((σ : (a : Fin n) → Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2)) =
      x2

Tactic:
simp [hlt.le]

Premises used: LT.lt.le
-- Module: Mathlib.GroupTheory.Perm.Fin
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
hlt : x2 < x1
hle :
  LE.le (α := Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x2 : Fin n) ((Equiv.symm σ : (a : Fin n) → Fin n) x1 : Fin n)
⊢ ∃ (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

Tactic:
exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩
-- Module: Mathlib.GroupTheory.Perm.Fin
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

Tactic:
have hφD : D.image (fun x ↦ ⟨σ x.1 ⊔ σ x.2, σ x.1 ⊓ σ x.2⟩) = D := by
    ext ⟨x1, x2⟩
    suffices (∃ a, ∃ b < a, σ a ⊔ σ b = x1 ∧ σ a ⊓ σ b = x2) ↔ x2 < x1 by simpa [hD]
    refine ⟨?_, fun hlt ↦ ?_⟩
    · rintro ⟨i, j, hij, rfl, rfl⟩
      exact inf_le_sup.lt_of_ne <| by simp [hij.ne.symm]
    obtain hlt' | hle := lt_or_ge (σ.symm x1) (σ.symm x2)
    · exact ⟨_, _, hlt', by simp [hlt.le]⟩
    exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩