ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ 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) ^ card (support f)
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
⊢ ↑Perm.sign (swap x (↑f x) * (swap x (↑f x) * f)) = -(-1) ^ card (support f)
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]
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
h : swap x (↑f x) * f = 1
⊢ ↑Perm.sign (swap x (↑x✝ x) * (swap x (↑x✝ x) * x✝)) = -(-1) ^ card (support x✝)
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ 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) ^ card (support f)
dsimp only
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
h : swap x (↑f x) * f = 1
⊢ -1 * 1 = -(-1) ^ 2
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
h : swap x (↑f x) * f = 1
⊢ ↑Perm.sign (swap x (↑x✝ x) * (swap x (↑x✝ x) * x✝)) = -(-1) ^ card (support x✝)
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]
no goals
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
h : swap x (↑f x) * f = 1
⊢ -1 * 1 = -(-1) ^ 2
rfl
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
⊢ x✝.trans (swap x (↑x✝ x)) = Equiv.refl α
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
⊢ swap x (↑f x) * f = 1
simp only [mul_def, one_def]
no goals
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ↑f (↑f x) = x
⊢ x✝.trans (swap x (↑x✝ x)) = Equiv.refl α
rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap]
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
⊢ ↑Perm.sign (swap x (↑f x) * (swap x (↑f x) * f)) = -(-1) ^ card (support f)
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
⊢ ↑Perm.sign (swap x (↑f x) * (swap x (↑f x) * f)) = -(-1) ^ card (support f)
have h : card (support (swap x (f x) * f)) + 1 = card (support f) := 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]
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
this : card (support (swap x (↑f x) * f)) < card (support f)
⊢ ↑Perm.sign (swap x (↑f x) * (swap x (↑f x) * f)) = -(-1) ^ card (support f)
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
⊢ ↑Perm.sign (swap x (↑f x) * (swap x (↑f x) * f)) = -(-1) ^ card (support f)
have : card (support (swap x (f x) * f)) < card (support f) :=
  card_support_swap_mul hx.1
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
this : card (support (swap x (↑f x) * f)) < card (support f)
⊢ ↑Perm.sign (swap x (↑x✝ x) * (swap x (↑x✝ x) * x✝)) = -(-1) ^ card (support x✝)
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
this : card (support (swap x (↑f x) * f)) < card (support f)
⊢ ↑Perm.sign (swap x (↑f x) * (swap x (↑f x) * f)) = -(-1) ^ card (support f)
dsimp only
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
this : card (support (swap x (↑f x) * f)) < card (support f)
⊢ -1 * -(-1) ^ card (support (swap x (↑x✝ x) * x✝)) = -(-1) ^ (card (support (swap x (↑f x) * f)) + 1)
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
this : card (support (swap x (↑f x) * f)) < card (support f)
⊢ ↑Perm.sign (swap x (↑x✝ x) * (swap x (↑x✝ x) * x✝)) = -(-1) ^ card (support x✝)
rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
no goals
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
h : card (support (swap x (↑f x) * f)) + 1 = card (support f)
this : card (support (swap x (↑f x) * f)) < card (support f)
⊢ -1 * -(-1) ^ card (support (swap x (↑x✝ x) * x✝)) = -(-1) ^ (card (support (swap x (↑f x) * f)) + 1)
simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]
no goals
ι : Type ?u.914072
α : Type u_1
β : Type ?u.914078
f✝ g : Perm α
x✝¹ y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : Perm α
f : Perm α := x✝
hf : IsCycle x✝
x : α
hx : ↑x✝ x ≠ x ∧ ∀ ⦃y : α⦄, ↑x✝ y ≠ y → SameCycle x✝ x y
h1 : ¬↑f (↑f x) = x
⊢ card (support (swap x (↑f x) * f)) + 1 = card (support f)
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]