ι : Type ?u.1642783
α : Type u_1
β : Type ?u.1642789
f g : Perm α
s t : Set α
a b x y : α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → SameCycle f x y) → (Set.BijOn (↑f⁻¹) s s ↔ Set.BijOn (↑f) s s)
ι : Type ?u.1642783
α : Type u_1
β : Type ?u.1642789
f g : Perm α
s t : Set α
a b x y : α
⊢ IsCycleOn f⁻¹ s ↔ IsCycleOn f s
simp only [IsCycleOn, sameCycle_inv, and_congr_left_iff]
no goals
ι : Type ?u.1642783
α : Type u_1
β : Type ?u.1642789
f g : Perm α
s t : Set α
a b x y : α
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → SameCycle f x y) → (Set.BijOn (↑f⁻¹) s s ↔ Set.BijOn (↑f) s s)
exact fun _ ↦ ⟨fun h ↦ Set.BijOn.perm_inv h, fun h ↦ Set.BijOn.perm_inv h⟩