G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement {g} S
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ IsComplement {g} S ↔ S = ⊤
refine'
  ⟨fun h => top_le_iff.mp fun x _ => _, fun h => (congr_arg _ h).mpr isComplement_singleton_top⟩
case intro.mk.mk.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
x : G
x✝ : x ∈ ⊤
z : G
h : IsComplement {z} S
y : G
property✝ : y ∈ S
hy : (fun x => ↑x.fst * ↑x.snd) ({ val := z, property := (_ : z = z) }, { val := y, property := property✝ }) = z * x
⊢ x ∈ S
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement {g} S
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S
obtain ⟨⟨⟨z, rfl : z = g⟩, y, _⟩, hy⟩ := h.2 (g * x)
no goals
case intro.mk.mk.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
x : G
x✝ : x ∈ ⊤
z : G
h : IsComplement {z} S
y : G
property✝ : y ∈ S
hy : (fun x => ↑x.fst * ↑x.snd) ({ val := z, property := (_ : z = z) }, { val := y, property := property✝ }) = z * x
⊢ x ∈ S
rwa [← mul_left_cancel hy]