G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
g : G
⊢ ∃ a, (fun x => ↑x.fst * ↑x.snd) a = g
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
⊢ IsComplement' H K
refine' ⟨mul_injective_of_disjoint h1, fun g => _⟩
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
g h k : G
hh : h ∈ ↑H
hk : k ∈ ↑K
hg : (fun x x_1 => x * x_1) h k = g
⊢ ∃ a, (fun x => ↑x.fst * ↑x.snd) a = g
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
g : G
⊢ ∃ a, (fun x => ↑x.fst * ↑x.snd) a = g
obtain ⟨h, k, hh, hk, hg⟩ := Set.eq_univ_iff_forall.mp h2 g
no goals
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
h1 : Disjoint H K
h2 : ↑H * ↑K = Set.univ
g h k : G
hh : h ∈ ↑H
hk : k ∈ ↑K
hg : (fun x x_1 => x * x_1) h k = g
⊢ ∃ a, (fun x => ↑x.fst * ↑x.snd) a = g
exact ⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩