case refine'_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
⊢ Set.Nonempty S

case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b

case refine'_3
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∃ g, S = {g}) → IsComplement S ⊤
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ IsComplement S ⊤ ↔ ∃ g, S = {g}
refine'
  ⟨fun h => Set.exists_eq_singleton_iff_nonempty_subsingleton.mpr ⟨_, fun a ha b hb => _⟩, _⟩
case refine'_1.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : ↑S × ↑⊤
h✝ : (fun x => ↑x.fst * ↑x.snd) a = 1
⊢ Set.Nonempty S
case refine'_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
⊢ Set.Nonempty S
obtain ⟨a, _⟩ := h.2 1
no goals
case refine'_1.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : ↑S × ↑⊤
h✝ : (fun x => ↑x.fst * ↑x.snd) a = 1
⊢ Set.Nonempty S
exact ⟨a.1.1, a.1.2⟩
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this :
  ({ val := a, property := ha }, { val := a⁻¹, property := (_ : a⁻¹ ∈ ⊤) }) =
    ({ val := b, property := hb }, { val := b⁻¹, property := (_ : b⁻¹ ∈ ⊤) })
⊢ a = b
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : G
ha : a ∈ S
b : G
hb : b ∈ S
⊢ a = b
have : (⟨⟨a, ha⟩, ⟨_, mem_top a⁻¹⟩⟩ : S × (⊤ : Set G)) = ⟨⟨b, hb⟩, ⟨_, mem_top b⁻¹⟩⟩ :=
  h.1 ((mul_inv_self a).trans (mul_inv_self b).symm)
no goals
case refine'_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement S ⊤
a : G
ha : a ∈ S
b : G
hb : b ∈ S
this :
  ({ val := a, property := ha }, { val := a⁻¹, property := (_ : a⁻¹ ∈ ⊤) }) =
    ({ val := b, property := hb }, { val := b⁻¹, property := (_ : b⁻¹ ∈ ⊤) })
⊢ a = b
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).1
case refine'_3.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
T : Set G
g : G
⊢ IsComplement {g} ⊤
case refine'_3
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∃ g, S = {g}) → IsComplement S ⊤
rintro ⟨g, rfl⟩
no goals
case refine'_3.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
T : Set G
g : G
⊢ IsComplement {g} ⊤
exact isComplement_singleton_top