no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
x : Quotient α β
φ : Quotient α β → β
hφ : Function.RightInverse φ Quotient.mk'
⊢ orbit x = MulAction.orbit α (φ x)
conv_lhs => rw [← hφ x]