ι : Type ?u.1643430
α : Type u_1
β : Type ?u.1643436
f g : Perm α
s t : Set α
a b x✝ y✝ : α
h : IsCycleOn f s
x : α
hx : x ∈ ↑g⁻¹ ⁻¹' s
y : α
hy : y ∈ ↑g⁻¹ ⁻¹' s
⊢ SameCycle (g * f * g⁻¹) x y
ι : Type ?u.1643430
α : Type u_1
β : Type ?u.1643436
f g : Perm α
s t : Set α
a b x✝ y✝ : α
h : IsCycleOn f s
x : α
hx : x ∈ ↑g '' s
y : α
hy : y ∈ ↑g '' s
⊢ SameCycle (g * f * g⁻¹) x y
rw [← preimage_inv] at hx hy
no goals
ι : Type ?u.1643430
α : Type u_1
β : Type ?u.1643436
f g : Perm α
s t : Set α
a b x✝ y✝ : α
h : IsCycleOn f s
x : α
hx : x ∈ ↑g⁻¹ ⁻¹' s
y : α
hy : y ∈ ↑g⁻¹ ⁻¹' s
⊢ SameCycle (g * f * g⁻¹) x y
convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> rw [apply_inv_self]