subgroup_product_mul_closed

forall (G : Sort u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (group_args : @GroupLawArgs.{u} G one mul inv), forall (Hpred : forall (x : G), Prop), forall (N : forall (x : G), Prop), forall (h_args : @SubgroupLawArgs.{u} G one mul inv Hpred), forall (n_normal : @NormalSubgroupLawArgs.{u} G one mul inv N), forall (x : G), forall (y : G), forall (hx : @SubgroupProductPred.{u} G mul Hpred N x), forall (hy : @SubgroupProductPred.{u} G mul Hpred N y), @SubgroupProductPred.{u} G mul Hpred N (mul x y)

fun G => fun one => fun mul => fun inv => fun group_args => fun Hpred => fun N => fun h_args => fun n_normal => fun x => fun y => fun hx => fun hy => hx (@SubgroupProductPred.{u} G mul Hpred N (mul x y)) (fun (h1 : G) => fun (n1 : G) => fun (hh1 : Hpred h1) => fun (hn1 : N n1) => fun (hex : @Eq.{u} G (mul h1 n1) x) => hy (@SubgroupProductPred.{u} G mul Hpred N (mul x y)) (fun (h2 : G) => fun (n2 : G) => fun (hh2 : Hpred h2) => fun (hn2 : N n2) => fun (hey : @Eq.{u} G (mul h2 n2) y) => @subgroup_product_intro.{u} G mul Hpred N (mul x y) (mul h1 h2) (mul (mul (mul (inv h2) n1) h2) n2) (@subgroup_mul_closed.{u} G one mul inv Hpred h_args h1 h2 hh1 hh2) (@subgroup_mul_closed.{u} G one mul inv N (@normal_subgroup_laws.{u} G one mul inv N n_normal) (mul (mul (inv h2) n1) h2) n2 (@normal_inv_conj_closed.{u} G one mul inv group_args N n_normal h2 n1 hn1) hn2) (@eq_trans.{u} G (mul (mul h1 h2) (mul (mul (mul (inv h2) n1) h2) n2)) (mul (mul h1 n1) (mul h2 n2)) (mul x y) (@group_product_mul_reassoc.{u} G one mul inv group_args h1 n1 h2 n2) (@eq_congr2.{u,u,u} G G G mul (mul h1 n1) x (mul h2 n2) y hex hey))))