G : Type u_1
inst✝¹ : Group G
α : Type ?u.40758
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
⊢ ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K) → a = b
G : Type u_1
inst✝¹ : Group G
α : Type ?u.40758
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
⊢ a ≠ b → Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
contrapose!
G : Type u_1
inst✝¹ : Group G
α : Type ?u.40758
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
h : ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
⊢ a = b
G : Type u_1
inst✝¹ : Group G
α : Type ?u.40758
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
⊢ ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K) → a = b
intro h
no goals
G : Type u_1
inst✝¹ : Group G
α : Type ?u.40758
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
h : ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
⊢ a = b
simpa [out_eq'] using mk_eq_of_doset_eq (eq_of_not_disjoint h)