G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ IsComplement S {g} ↔ S = ⊤
refine'
  ⟨fun h => top_le_iff.mp fun x _ => _, fun h => h ▸ isComplement_top_singleton⟩
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * g
⊢ x ∈ S
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
⊢ x ∈ S
obtain ⟨y, hy⟩ := h.2 (x * g)
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * ↑y.snd
⊢ x ∈ S
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * g
⊢ x ∈ S
conv_rhs at hy => rw [← show y.2.1 = g from y.2.2]
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * ↑y.snd
⊢ ↑y.fst ∈ S
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * ↑y.snd
⊢ x ∈ S
rw [← mul_right_cancel hy]
no goals
case intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
h : IsComplement S {g}
x : G
x✝ : x ∈ ⊤
y : ↑S × ↑{g}
hy : (fun x => ↑x.fst * ↑x.snd) y = x * ↑y.snd
⊢ ↑y.fst ∈ S
exact y.1.2