G : Type u_1
inst✝¹ : Group G
α : Type ?u.26004
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
⊢ Setoid.r a b ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
G : Type u_1
inst✝¹ : Group G
α : Type ?u.26004
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
⊢ mk H K a = mk H K b ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
rw [Quotient.eq'']
no goals
G : Type u_1
inst✝¹ : Group G
α : Type ?u.26004
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
⊢ Setoid.r a b ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
apply rel_iff