-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ #f.support :=
  let ⟨x, hx⟩ := hf
  calc
    Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f))

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
⊢ swap x (f x) * f = 1

Tactic:
simp only [mul_def, one_def]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
⊢ Equiv.trans f (swap x (f x)) = Equiv.refl α

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
h : #(swap x (f x) * f).support + 1 = #f.support
this : #(swap x (f x) * f).support < #f.support
⊢ -1 * -(-1) ^ #(swap x (f x) * f).support = -(-1) ^ (#(swap x (f x) * f).support + 1)

Tactic:
simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ -1 * 1 = -(-1) ^ 2

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Tactic:
have h : #(swap x (f x) * f).support + 1 = #f.support := by
  rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
    card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
h : #(swap x (f x) * f).support + 1 = #f.support
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(swap x (f x) * f).support + 1 = #f.support

Tactic:
rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
  card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
h : #(swap x (f x) * f).support + 1 = #f.support
this : #(swap x (f x) * f).support < #f.support
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Tactic:
rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
h : #(swap x (f x) * f).support + 1 = #f.support
this : #(swap x (f x) * f).support < #f.support
⊢ -1 * -(-1) ^ #(swap x (f x) * f).support = -(-1) ^ (#(swap x (f x) * f).support + 1)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Tactic:
rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
  hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ -1 * 1 = -(-1) ^ 2

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
⊢ Equiv.trans f (swap x (f x)) = Equiv.refl α

Tactic:
rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
h : #(swap x (f x) * f).support + 1 = #f.support
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Tactic:
have : #(swap x (f x) * f).support < #f.support := card_support_swap_mul hx.1

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
h : #(swap x (f x) * f).support + 1 = #f.support
this : #(swap x (f x) * f).support < #f.support
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Tactic:
have h : swap x (f x) * f = 1 := by
  simp only [mul_def, one_def]
  rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
⊢ Perm.sign f = Perm.sign (swap x (f x) * (swap x (f x) * f))

Tactic:
rw [← mul_assoc, mul_def, mul_def, swap_swap, trans_refl]

Result:
no goals