case h.e'_4
ι : Type ?u.1652962
α : Type u_1
β : Type ?u.1652968
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hx : ↑f x ∈ s
⊢ x = ↑f⁻¹ (↑f x)
ι : Type ?u.1652962
α : Type u_1
β : Type ?u.1652968
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hx : ↑f x ∈ s
⊢ x ∈ s
convert hf.1.perm_inv.1 hx
no goals
case h.e'_4
ι : Type ?u.1652962
α : Type u_1
β : Type ?u.1652968
f g : Perm α
s t : Set α
a b x y : α
hf : IsCycleOn f s
hx : ↑f x ∈ s
⊢ x = ↑f⁻¹ (↑f x)
rw [inv_apply_self]