G : Type u_1
inst✝¹ : Group G
α : Type ?u.10571
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
G : Type u_1
inst✝¹ : Group G
α : Type ?u.10571
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
rw [disjoint_comm] at h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.10571
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
ha : a ∈ doset b ↑H ↑K
⊢ doset a ↑H ↑K = doset b ↑H ↑K
G : Type u_1
inst✝¹ : Group G
α : Type ?u.10571
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
have ha : a ∈ doset b H K := mem_doset_of_not_disjoint h
no goals
G : Type u_1
inst✝¹ : Group G
α : Type ?u.10571
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
ha : a ∈ doset b ↑H ↑K
⊢ doset a ↑H ↑K = doset b ↑H ↑K
apply doset_eq_of_mem ha