feat(group_theory/complement): is_complement'.sup_eq_top (#10230)

If `H` and `K` are complementary subgroups, then `H ⊔ K = ⊤`.

src/group_theory/complement.lean

@@ -210,6 +210,20 @@ mem_right_transversals_iff_exists_unique_quotient_mk'_eq.trans
 { rintros ⟨_, q₁, rfl⟩ ⟨_, q₂, rfl⟩ hg,
   rw (q₁.out_eq'.symm.trans hg).trans q₂.out_eq' }, λ q, ⟨⟨q.out', q, rfl⟩, quotient.out_eq' q⟩⟩⟩⟩
 
+lemma is_complement'.is_compl (h : is_complement' H K) : is_compl H K :=
+begin
+  refine ⟨λ g ⟨p, q⟩, let x : H × K := ⟨⟨g, p⟩, 1⟩, y : H × K := ⟨1, g, q⟩ in subtype.ext_iff.mp
+    (prod.ext_iff.mp (show x = y, from h.1 ((mul_one g).trans (one_mul g).symm))).1, λ g _, _⟩,
+  obtain ⟨⟨h, k⟩, rfl⟩ := h.2 g,
+  exact subgroup.mul_mem_sup h.2 k.2,
+end
+
+lemma is_complement'.sup_eq_top (h : subgroup.is_complement' H K) : H ⊔ K = ⊤ :=
+h.is_compl.sup_eq_top
+
+lemma is_complement'.disjoint (h : is_complement' H K) : disjoint H K :=
+h.is_compl.disjoint
+
 lemma is_complement.card_mul [fintype G] [fintype S] [fintype T] (h : is_complement S T) :
   fintype.card S * fintype.card T = fintype.card G :=
 (fintype.card_prod _ _).symm.trans (fintype.card_of_bijective h)
@@ -218,10 +232,6 @@ lemma is_complement'.card_mul [fintype G] [fintype H] [fintype K] (h : is_comple
   fintype.card H * fintype.card K = fintype.card G :=
 h.card_mul
 
-lemma is_complement'.disjoint (h : is_complement' H K) : disjoint H K :=
-λ g hg, let x : H × K := ⟨⟨g, hg.1⟩, 1⟩, y : H × K := ⟨1, ⟨g, hg.2⟩⟩ in subtype.ext_iff.mp
-  (prod.ext_iff.mp (h.1 (show x.1.1 * _ = y.1.1 * _, from (mul_one g).trans (one_mul g).symm))).1
-
 lemma is_complement'_of_card_mul_and_disjoint [fintype G] [fintype H] [fintype K]
   (h1 : fintype.card H * fintype.card K = fintype.card G) (h2 : disjoint H K) :
   is_complement' H K :=