Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype.
Require Import div path bigop prime finset fingroup morphism quotient.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section Ex10.

Variable gT : finGroupType.
Implicit Types G H K : {group gT}.
Open Scope group_scope.

Lemma ex10_1 x G H : x \in H  -> H \subset G -> x \in G.
(*D*) Proof. by move=> xH /subsetP ->. Qed.

Lemma ex10_2 x y G H : x \in H :* y  -> H \subset G -> x \in G :* y.
(*D*) Proof. by move=> xHy; rewrite -(rcosetS y) => /subsetP/(_ _ xHy). Qed.

Lemma ex10_3 G H : H <| G -> H * G = G * H.
(*D*) Proof. by case/andP=> sHG /normC ->. Qed.

(* Prove this without using the lemma ltn_quotient, and remember that
   quotient is a morphism *)
Lemma ex10_ltn_quotient A H :
  1 < #|H| -> H <| A -> 0 < #|A| - #|A / H|.
Proof.
(*D*) rewrite subn_gt0 cardG_gt1=> ntH /andP[sHA _].
(*D*) by rewrite ltn_morphim // ker_coset (setIidPr sHA) proper1G.
Qed.

(* Give a look at: Search _ "imset" "P". and at the notation of 
   set comprehension. Also look at "bigcup" and subsetP *)
Lemma ex10_4 G H : H \subset 'N(G) -> [set g ^ h | g <- G , h <- H] = G.
Proof.
(*D*) move=> nHG; apply/eqP.
(*D*) rewrite curry_imset2r eqEsubset; apply/andP; split.
(*D*)   by apply/bigcupsP=> h hH; rewrite -/(G :^ h) (normsP nHG).
(*D*) apply: subset_trans _ (bigcup_sup 1 _) => //; apply/subsetP=> x xG.
(*D*) by apply/imsetP; exists x; rewrite // conjg1.
Qed.

(* Prove the following lemma. Give a look at setX, leq_imset_card,
   subset_leq_card and imsetP *)
Lemma ex10_ineq G H K : #|G : H :&: K| <= #|G : H| * #|G : K|.
Proof.
(*D*) rewrite -cardsX.
(*D*) pose f x : {set gT} := let: (Hg, Kg) := x in Hg :&: Kg.
(*D*) apply: leq_trans _ (leq_imset_card f _).
(*D*) apply/subset_leq_card/subsetP=> x /imsetP[g gG ->].
(*D*) apply/imsetP=> /=; exists (H :* g, K :* g).
(*D*)   by rewrite inE /= !mem_rcosets -[g]mul1g ?mem_mulg.
(*D*) apply/setP=> HKg; apply/imsetP/idP.
(*D*)   by case=> z /setIP[zK zH ->]; rewrite inE !mem_mulg // inE.
(*D*) case/setIP=> /rcosetP[a aH ->]; rewrite mem_rcoset mulgK => aK.
(*D*) by exists a; rewrite // inE ?aH.
Qed.

(* Advanced: read in the documentation (page 46) what happens
   when one writes 'rewrite (lem1, lem2, lem3)' and use it to solve
   the following identity. *)
Lemma Hall_Witt_identity (x y z : gT) :
   [~ x, y^-1, z] ^ y * [~ y, z^-1, x] ^ z * [~ z, x^-1, y] ^ x = 1.
Proof.
(*D*) rewrite !commgEr !conjgE !invMg.
(*D*) by rewrite !(mulg1, mul1g, invg1, mulVg, mulgV, invgK, mulgK, mulgKV, invMg, mulgA).
Qed.

End Ex10.