case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.4114
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
k h a : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ doset ((fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) h a) k) ↑H ↑K = doset a ↑H ↑K
G : Type u_1
inst✝¹ : Group G
α : Type ?u.4114
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
hb : b ∈ doset a ↑H ↑K
⊢ doset b ↑H ↑K = doset a ↑H ↑K
obtain ⟨_, k, ⟨h, a, hh, rfl : _ = _, rfl⟩, hk, rfl⟩ := hb
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.4114
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
k h a : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ doset ((fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) h a) k) ↑H ↑K = doset a ↑H ↑K
rw [doset, doset, ← Set.singleton_mul_singleton, ← Set.singleton_mul_singleton, mul_assoc,
  mul_assoc, Subgroup.singleton_mul_subgroup hk, ← mul_assoc, ← mul_assoc,
  Subgroup.subgroup_mul_singleton hh]