G : Type u_1
inst✝¹ : Group G
α : Type ?u.39521
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
G : Type u_1
inst✝¹ : Group G
α : Type ?u.39521
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ mk H K a = mk H K b
rw [eq]
no goals
G : Type u_1
inst✝¹ : Group G
α : Type ?u.39521
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
exact mem_doset.mp (h.symm ▸ mem_doset_self H K b)