α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b ↔ b * a⁻¹ ∈ s
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b = (b * a⁻¹ ∈ s)
simp only [eq_iff_iff]
no goals
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b ↔ b * a⁻¹ ∈ s
apply rightRel_apply