proposition: Theorem third_isom : {f : {morphism (G / H) / (K / H) >-> coset_of K} | 'injm f & forall A : {set gT}, A \subset G -> f @* (A / H / (K / H)) = A / K}.
proof: Proof. have [[sKG nKG] [sHG nHG]] := (andP snKG, andP snHG). have sHker: 'ker (coset H) \subset 'ker (restrm nKG (coset K)). by rewrite ker_restrm !ker_coset subsetI sHG. have:= first_isom_loc (factm_morphism sHker nHG) (subxx _) => /=. rewrite ker_factm_loc ker_restrm ker_coset !(setIidPr sKG) /= -!quotientE. case=> f injf im_f; exists f => // A sAG; rewrite im_f ?morphimS //. by rewrite morphim_factm morphim_restrm (setIidPr sAG). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype prime finset fingroup morphism) mathcomp(automorphism)