awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
H :
  (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
            (a : Fin n) → Fin n)
          ((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α)))) :
      ℕ)
⊢ (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
            (a : Fin n) → Fin n)
          ((e : (a : α) → Fin n) ((e.symm.trans f : (a : Fin n) → α) x_1))) :
      ℕ)

Tactic:
rw [trans_apply]

Premises used: Equiv.trans_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
H :
  (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
            (a : Fin n) → Fin n)
          ((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α)))) :
      ℕ)
⊢ (↑(((e.symm.trans (Equiv.trans f (swap x ((f : (a : α) → α) x)))).trans e : (a : Fin n) → Fin n) x_1) : ℕ) =
    (↑((((e.symm.trans f).trans e).trans
              (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x))) :
            (a : Fin n) → Fin n)
          x_1) :
      ℕ)

Tactic:
repeat (rw [trans_apply])

Premises used: Equiv.trans_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
H :
  (↑((e : (a : α) → Fin n)
          (if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (f : (a : α) → α) x
          else
            if (e.symm : (a : Fin n) → α) x_1 = x then x else (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ) =
    (↑(if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (e : (a : α) → Fin n) ((f : (a : α) → α) x)
        else
          if (e.symm : (a : Fin n) → α) x_1 = x then (e : (a : α) → Fin n) x
          else (e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ)
⊢ (↑((e : (a : α) → Fin n)
          ((swap x ((f : (a : α) → α) x) : (a : α) → α) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) : α))) :
      ℕ) =
    (↑(((swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : Perm (Fin n)) :
            (a : Fin n) → Fin n)
          ((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α)))) :
      ℕ)

Tactic:
simp [swap, swapCore]

Premises used: Equiv.swapCore, Equiv.swap
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
pos :
  (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
    (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ) = (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ)
pos₁ :
  ¬(f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
    (e.symm : (a : Fin n) → α) x_1 = x → (↑((e : (a : α) → Fin n) x) : ℕ) = (↑((e : (a : α) → Fin n) x) : ℕ)
neg :
  ¬(f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x →
    ¬(e.symm : (a : Fin n) → α) x_1 = x →
      (↑((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) : ℕ) =
        (↑((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) : ℕ)
⊢ (↑((e : (a : α) → Fin n)
          (if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (f : (a : α) → α) x
          else
            if (e.symm : (a : Fin n) → α) x_1 = x then x else (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ) =
    (↑(if (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x then (e : (a : α) → Fin n) ((f : (a : α) → α) x)
        else
          if (e.symm : (a : Fin n) → α) x_1 = x then (e : (a : α) → Fin n) x
          else (e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) :
      ℕ)

Tactic:
split_ifs
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
h_1 : (f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x
⊢ (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ) = (↑((e : (a : α) → Fin n) ((f : (a : α) → α) x)) : ℕ)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
h_1 : ¬(f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x
h_2 : (e.symm : (a : Fin n) → α) x_1 = x
⊢ (↑((e : (a : α) → Fin n) x) : ℕ) = (↑((e : (a : α) → Fin n) x) : ℕ)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_2 : α), (f : (a : α) → α) x_2 ≠ x_2 → x_2 ∈ x :: l
hfx : ¬x = (f : (a : α) → α) x
hy : ∀ (y : α), (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y → y ∈ l
x_1 : Fin n
h_1 : ¬(f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α) = x
h_2 : ¬(e.symm : (a : Fin n) → α) x_1 = x
⊢ (↑((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) : ℕ) =
    (↑((e : (a : α) → Fin n) ((f : (a : α) → α) ((e.symm : (a : Fin n) → α) x_1 : α))) : ℕ)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
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)

Tactic:
have : (e.symm.trans (swap x (f x) * f)).trans e =
          swap (e x) (e (f x)) * (e.symm.trans f).trans e := by
        ext
        rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
        repeat (rw [trans_apply])
        simp [swap, swapCore]
        split_ifs <;> rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
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
this :
  (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)
⊢ Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) ((f : (a : α) → α) x) : Fin n)

Tactic:
have hefx : e x ≠ e (f x) := mt e.injective.eq_iff.1 hfx
-- Module: Mathlib.GroupTheory.Perm.Sign
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
this :
  (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)
hefx : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) ((f : (a : α) → α) x) : Fin n)
neg : signAux ((e.symm.trans f).trans e) = -(-1 * signAux ((e.symm.trans f).trans e))
⊢ 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:
rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]

Premises used: Equiv.Perm.signAux_swap, if_neg, Equiv.Perm.signAux_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
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
this :
  (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)
hefx : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) ((f : (a : α) → α) x) : Fin n)
⊢ signAux ((e.symm.trans f).trans e) = -(-1 * signAux ((e.symm.trans f).trans e))

Tactic:
simp only [neg_neg, one_mul, neg_mul]

Premises used: neg_neg, neg_mul, one_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
rcases :
  ∀ (n : ℕ) (e : α ≃ Fin n),
    HEq (α := (∀ (x : α), x ∈ ⟦l₁⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₁⟧) ↦ signAux2 l₁ f (β :=
      (∀ (x : α), x ∈ ⟦l₂⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₂⟧) ↦ signAux2 l₂ f
⊢ HEq (α := (∀ (x : α), x ∈ ⟦l₁⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₁⟧) ↦ signAux2 l₁ f (β := (∀ (x : α), x ∈ ⟦l₂⟧) → ℤˣ)
    fun (x : ∀ (x : α), x ∈ ⟦l₂⟧) ↦ signAux2 l₂ f

Tactic:
rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
⊢ HEq (α := (∀ (x : α), x ∈ ⟦l₁⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₁⟧) ↦ signAux2 l₁ f (β := (∀ (x : α), x ∈ ⟦l₂⟧) → ℤˣ)
    fun (x : ∀ (x : α), x ∈ ⟦l₂⟧) ↦ signAux2 l₂ f

Tactic:
Function.hfunext (forall_congr fun _ ↦ propext h.mem_iff) fun h₁ h₂ _ ↦ ?_

Premises used: propext, Function.hfunext, List.Perm.mem_iff, forall_congr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
refine : ∀ (h₁ : ∀ (x : α), x ∈ ⟦l₁⟧) (h₂ : ∀ (x : α), x ∈ ⟦l₂⟧), h₁ ≍ h₂ → signAux2 l₁ f ≍ signAux2 l₂ f
⊢ HEq (α := (∀ (x : α), x ∈ ⟦l₁⟧) → ℤˣ) fun (x : ∀ (x : α), x ∈ ⟦l₁⟧) ↦ signAux2 l₁ f (β := (∀ (x : α), x ∈ ⟦l₂⟧) → ℤˣ)
    fun (x : ∀ (x : α), x ∈ ⟦l₂⟧) ↦ signAux2 l₂ f

Tactic:
refine Function.hfunext (forall_congr fun _ ↦ propext h.mem_iff) fun h₁ h₂ _ ↦ ?_

Premises used: propext, Function.hfunext, List.Perm.mem_iff, forall_congr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
f : Perm α
s : Multiset α
l₁ l₂ : List α
h : l₁ ≈ l₂
n : ℕ
e : α ≃ Fin n
h₁ : ∀ (x : α), x ∈ ⟦l₁⟧
h₂ : ∀ (x : α), x ∈ ⟦l₂⟧
h_1 : h₁ ≍ h₂
rw : signAux ((e.symm.trans f).trans e) ≍ signAux2 l₂ f
rw₁ rw₂ : signAux ((e.symm.trans f).trans e) ≍ signAux ((e.symm.trans f).trans e)
⊢ signAux2 l₁ f ≍ signAux2 l₂ f

Tactic:
rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]

Premises used: Equiv.Perm.signAux_eq_signAux2
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
obtain :
  ∀ (n : ℕ) (e : α ≃ Fin n),
    (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin α

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1

Tactic:
?_
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
n : ℕ
e : α ≃ Fin n
h :
  ∀ (l : List α) (hs : ∀ (x : α), x ∈ ⟦l⟧),
    (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1

Tactic:
induction s using Quotient.inductionOn with | _ l => ?_
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
h : signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1
⊢ (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) ↦ (swap x y).signAux3 hs = -1

Tactic:
change
    signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧
    Pairwise fun x y => signAux2 l (swap x y) = -1

Premises used: Equiv.Perm.signAux2, HMul.hMul, Equiv.swap, Pairwise, OfNat.ofNat, Eq, Neg.neg
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
h : Fin n
⊢ Eq (α := Fin n) (((e.symm.trans (f * g)).trans e : (a : Fin n) → Fin n) h : Fin n)
    (((e.symm.trans f).trans e * (e.symm.trans g).trans e : (a : Fin n) → Fin n) h : Fin n)

Tactic:
simp [mul_apply]

Premises used: Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
⊢ (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e

Tactic:
have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e :=
    Equiv.ext fun h => by simp [mul_apply]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
h : signAux2 l (f * g) = signAux2 l f * signAux2 l g
h₁ : Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun (x y : α) ↦ signAux2 l (swap x y) = -1

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
h : signAux ((e.symm.trans (f * g)).trans e) = signAux2 l f * signAux2 l g
h₁ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux2 l g
h₂ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
h₃ :
  signAux ((e.symm.trans f).trans e * (e.symm.trans g).trans e) =
    signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
h₄ h₅ :
  signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e) =
    signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g

Tactic:
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]

Premises used: Equiv.Perm.signAux_eq_signAux2, Equiv.Perm.signAux_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
⊢ Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) y : Fin n)

Tactic:
rw [← e.injective.ne_iff] at hxy

Premises used: Function.Injective.ne_iff, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) y : Fin n)
h : signAux ((e.symm.trans (swap x y)).trans e) = -1
h₁ : signAux (n := n) (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) y)) = -1
h₂ h₃ : Eq (α := ℤˣ) (-1) (-1)
⊢ signAux2 l (swap x y) = -1

Tactic:
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]

Premises used: Equiv.Perm.signAux_swap, Equiv.Perm.signAux_eq_signAux2, Equiv.symm_trans_swap_trans
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
s : Multiset α
t : Multiset β
hs : ∀ (x : α), x ∈ s
ht : ∀ (x : β), x ∈ t
h :
  ∀ (a : List β) (b : List α) (hs : ∀ (x : α), x ∈ ⟦b⟧) (ht : ∀ (x : β), x ∈ ⟦a⟧),
    signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Tactic:
induction t, s using Quotient.inductionOn₂
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
h : signAux2 a ((e.symm.trans f).trans e) = signAux2 b f
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Tactic:
change signAux2 _ _ = signAux2 _ _

Premises used: Equiv.Perm.signAux2
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
h : ∀ (n : ℕ) (e' : β ≃ Fin n), signAux2 a ((e.symm.trans f).trans e) = signAux2 b f
⊢ signAux2 a ((e.symm.trans f).trans e) = signAux2 b f

Tactic:
rcases Finite.exists_equiv_fin β with ⟨n, ⟨e'⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
n : ℕ
e' : β ≃ Fin n
h :
  signAux ((e'.symm.trans ((e.symm.trans f).trans e)).trans e') =
    signAux (((e.trans e').symm.trans f).trans (e.trans e'))
⊢ signAux2 a ((e.symm.trans f).trans e) = signAux2 b f

Tactic:
rw [← signAux_eq_signAux2 _ _ e' fun _ _ => ht _,
    ← signAux_eq_signAux2 _ _ (e.trans e') fun _ _ => hs _]

Premises used: Equiv.trans, Equiv.Perm.signAux_eq_signAux2
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
n : ℕ
e' : β ≃ Fin n
x : Fin n
⊢ Eq (α := Fin n) (((e'.symm.trans ((e.symm.trans f).trans e)).trans e' : (a : Fin n) → Fin n) x : Fin n)
    ((((e.trans e').symm.trans f).trans (e.trans e') : (a : Fin n) → Fin n) x : Fin n)

Tactic:
simp [symm_trans_apply]

Premises used: Equiv.symm_trans_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
n : ℕ
e' : β ≃ Fin n
⊢ signAux ((e'.symm.trans ((e.symm.trans f).trans e)).trans e') =
    signAux (((e.trans e').symm.trans f).trans (e.trans e'))

Tactic:
exact congr_arg signAux
    (Equiv.ext fun x => by simp [symm_trans_apply])

Premises used: Equiv.Perm.signAux, Equiv.ext, congr_arg
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (f * g) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)

Tactic:
map_mul sign f g

Premises used: Equiv.Perm.sign, map_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
rw :
  ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (g * f) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
rw₁ rw₂ :
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (Equiv.trans f g) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
rw [← mul_def, sign_mul]

Premises used: Equiv.Perm.mul_def, Equiv.Perm.sign_mul
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1) 1

Tactic:
map_one sign

Premises used: Equiv.Perm.sign, map_one
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (Equiv.refl α) : ℤˣ) (1 : ℤˣ)

Tactic:
map_one sign

Premises used: Equiv.Perm.sign, map_one
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw :
  Eq (α := ℤˣ) ((((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f)⁻¹ : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
rw₁ rw₂ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f⁻¹ : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
rw [map_inv sign f, Int.units_inv_eq_self]

Premises used: map_inv, Equiv.Perm.sign, Int.units_inv_eq_self
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
e : Perm α
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (Equiv.symm e) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) e : ℤˣ)

Tactic:
sign_inv e

Premises used: Equiv.Perm.sign_inv
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
x y : α
h : x ≠ y
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)

Tactic:
(signAux3_mul_and_swap 1 1 _ mem_univ).2 h

Premises used: Finset.mem_univ, Equiv.Perm.signAux3_mul_and_swap, And.right, Equiv.Perm.signAux3, OfNat.ofNat