Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit (Tutorial/Advanced/Algebra/Lecture3.lean)

State before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y ↔ y ∈ orbit G x
Tactic:
sorry
State after:
no goals