group_product_mul_reassoc

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 (h : G), forall (n : G), forall (k : G), forall (m : G), @Eq.{u} G (mul (mul h k) (mul (mul (mul (inv k) n) k) m)) (mul (mul h n) (mul k m))

fun G => fun one => fun mul => fun inv => fun group_args => fun h => fun n => fun k => fun m => @eq_trans.{u} G (mul (mul h k) (mul (mul (mul (inv k) n) k) m)) (mul (mul (mul h k) (mul (mul (inv k) n) k)) m) (mul (mul h n) (mul k m)) (@eq_symm.{u} G (mul (mul (mul h k) (mul (mul (inv k) n) k)) m) (mul (mul h k) (mul (mul (mul (inv k) n) k) m)) (@group_mul_assoc.{u} G one mul inv group_args (mul h k) (mul (mul (inv k) n) k) m)) (@eq_trans.{u} G (mul (mul (mul h k) (mul (mul (inv k) n) k)) m) (mul (mul h (mul k (mul (mul (inv k) n) k))) m) (mul (mul h n) (mul k m)) (@eq_congr_arg.{u,u} G G (fun (z : G) => mul z m) (mul (mul h k) (mul (mul (inv k) n) k)) (mul h (mul k (mul (mul (inv k) n) k))) (@group_mul_assoc.{u} G one mul inv group_args h k (mul (mul (inv k) n) k))) (@eq_trans.{u} G (mul (mul h (mul k (mul (mul (inv k) n) k))) m) (mul (mul h (mul n k)) m) (mul (mul h n) (mul k m)) (@eq_congr_arg.{u,u} G G (fun (z : G) => mul (mul h z) m) (mul k (mul (mul (inv k) n) k)) (mul n k) (@group_conj_slide.{u} G one mul inv group_args k n)) (@eq_trans.{u} G (mul (mul h (mul n k)) m) (mul (mul (mul h n) k) m) (mul (mul h n) (mul k m)) (@eq_congr_arg.{u,u} G G (fun (z : G) => mul z m) (mul h (mul n k)) (mul (mul h n) k) (@eq_symm.{u} G (mul (mul h n) k) (mul h (mul n k)) (@group_mul_assoc.{u} G one mul inv group_args h n k))) (@group_mul_assoc.{u} G one mul inv group_args (mul h n) k m))))