theorem Cosets.coset_eq_of_mem {G : Type u_1} [Group G] (H : Subgroup G) (a b : G) (hb : b ∈ a • ↑H) : a • ↑H = b • ↑H

theorem Cosets.mem_leftCoset_self {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : g ∈ g • ↑H

theorem Cosets.leftCosets_eq_or_disjoint {G : Type u_1} [Group G] (H : Subgroup G) (a b : G) : a • ↑H = b • ↑H ∨ Disjoint (a • ↑H) (b • ↑H)

theorem Cosets.leftCosets_partition {G : Type u_1} [Group G] (H : Subgroup G) : (∀ (g : G), ∃ (a : G), g ∈ a • ↑H) ∧ ∀ (a b : G), a • ↑H = b • ↑H ∨ Disjoint (a • ↑H) (b • ↑H)