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.2.1, a.2.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 := (_ : a⁻¹ ∈ ⊤) }, { val := a, property := ha }) =
    ({ val := b⁻¹, property := (_ : b⁻¹ ∈ ⊤) }, { val := b, property := hb })
⊢ 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 : (⟨⟨_, mem_top a⁻¹⟩, ⟨a, ha⟩⟩ : (⊤ : Set G) × S) = ⟨⟨_, mem_top b⁻¹⟩, ⟨b, hb⟩⟩ :=
  h.1 ((inv_mul_self a).trans (inv_mul_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 := (_ : a⁻¹ ∈ ⊤) }, { val := a, property := ha }) =
    ({ val := b⁻¹, property := (_ : b⁻¹ ∈ ⊤) }, { val := b, property := hb })
⊢ a = b
exact Subtype.ext_iff.mp (Prod.ext_iff.mp this).2
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_top_singleton