no goals
ι : Type ?u.819516
α✝ : Type ?u.819519
β : Type ?u.819522
f✝ g : Perm α✝
x✝ y : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
hffx : ↑f (↑f x) ≠ x
⊢ ↑(swap x (↑f x) * f) (↑f x) ≠ ↑f x
simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, if_neg hx, hx]
no goals
ι : Type ?u.819516
α✝ : Type ?u.819519
β : Type ?u.819522
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
hffx : ↑f (↑f x) ≠ x
y : α
hy : ↑(swap x (↑f x) * f) y ≠ y
i : ℤ
hi : ↑(f ^ i) x = y
⊢ ↑(f ^ (i - 1)) (↑f x) = ↑(f ^ (i - 1) * f ^ 1) x
simp
no goals
ι : Type ?u.819516
α✝ : Type ?u.819519
β : Type ?u.819522
f✝ g : Perm α✝
x✝ y✝ : α✝
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
f : Perm α
hf : IsCycle f
x : α
hx : ↑f x ≠ x
hffx : ↑f (↑f x) ≠ x
y : α
hy : ↑(swap x (↑f x) * f) y ≠ y
i : ℤ
hi : ↑(f ^ i) x = y
⊢ ↑(f ^ (i - 1) * f ^ 1) x = y
rwa [← zpow_add, sub_add_cancel]