subgroup_product_inv_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 (hx : @SubgroupProductPred.{u} G mul Hpred N x), @SubgroupProductPred.{u} G mul Hpred N (inv x)

fun G => fun one => fun mul => fun inv => fun group_args => fun Hpred => fun N => fun h_args => fun n_normal => fun x => fun hx => hx (@SubgroupProductPred.{u} G mul Hpred N (inv x)) (fun (h : G) => fun (n : G) => fun (hh : Hpred h) => fun (hn : N n) => fun (hex : @Eq.{u} G (mul h n) x) => @subgroup_product_intro.{u} G mul Hpred N (inv x) (inv h) (mul (mul h (inv n)) (inv h)) (@subgroup_inv_closed.{u} G one mul inv Hpred h_args h hh) (@normal_conj_closed.{u} G one mul inv N n_normal h (inv n) (@subgroup_inv_closed.{u} G one mul inv N (@normal_subgroup_laws.{u} G one mul inv N n_normal) n hn)) (@eq_trans.{u} G (mul (inv h) (mul (mul h (inv n)) (inv h))) (inv (mul h n)) (inv x) (@group_product_inv_reassoc.{u} G one mul inv group_args h n) (@eq_congr_arg.{u,u} G G inv (mul h n) x hex)))