G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
g : G
x✝ : g ∈ ⊤
⊢ g ∈ H ⊔ K
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
⊢ IsCompl H K
refine'
  ⟨disjoint_iff_inf_le.mpr fun g ⟨p, q⟩ =>
      let x : H × K := ⟨⟨g, p⟩, 1⟩
      let y : H × K := ⟨1, g, q⟩
      Subtype.ext_iff.mp
        (Prod.ext_iff.mp (show x = y from h.1 ((mul_one g).trans (one_mul g).symm))).1,
    codisjoint_iff_le_sup.mpr fun g _ => _⟩
case intro.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h✝ : IsComplement' H K
h : ↑↑H
k : ↑↑K
x✝ : (fun x => ↑x.fst * ↑x.snd) (h, k) ∈ ⊤
⊢ (fun x => ↑x.fst * ↑x.snd) (h, k) ∈ H ⊔ K
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h : IsComplement' H K
g : G
x✝ : g ∈ ⊤
⊢ g ∈ H ⊔ K
obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g
no goals
case intro.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h✝ : IsComplement' H K
h : ↑↑H
k : ↑↑K
x✝ : (fun x => ↑x.fst * ↑x.snd) (h, k) ∈ ⊤
⊢ (fun x => ↑x.fst * ↑x.snd) (h, k) ∈ H ⊔ K
exact Subgroup.mul_mem_sup h.2 k.2