case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
b a✝ : β
⊢ b ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' b = Quotient.mk'' a✝
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
b : β
x : Quotient α β
⊢ b ∈ orbit x ↔ Quotient.mk'' b = x
induction x using Quotient.inductionOn'
case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
b a✝ : β
⊢ b ∈ orbit (Quotient.mk'' a✝) ↔ Setoid.r b a✝
case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
b a✝ : β
⊢ b ∈ orbit (Quotient.mk'' a✝) ↔ Quotient.mk'' b = Quotient.mk'' a✝
rw [Quotient.eq'']
no goals
case h
α : Type u
β : Type v
γ : Type w
inst✝¹ : Group α
inst✝ : MulAction α β
b a✝ : β
⊢ b ∈ orbit (Quotient.mk'' a✝) ↔ Setoid.r b a✝
rfl