Mathlib.Algebra.Ring.ChineseRemainder

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Image
import Mathlib.Algebra.Group.Kernel.Quotient
import Mathlib.Algebra.Group.Kernel.Quotient.Mul
import Mathlib.Algebra.Group.Kernel.Quotient.Group
import Mathlib.Algebra.Group.FirstIsomorphism
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.FirstIsomorphism.Basic
import Mathlib.Algebra.Ring.FirstIsomorphism

def RingCrtPairMap.{p,u,v,w} :
  forall (R : Sort u), forall (RI : Sort v), forall (RJ : Sort w), forall (P : Sort p), forall (pair : forall (x : RI), forall (y : RJ), P), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (x : R), P :=
  fun R => fun RI => fun RJ => fun P => fun pair => fun modI => fun modJ => fun x => pair (modI x) (modJ x)

def RingCrtCombine.{u} :
  forall (R : Sort u), forall (add : forall (a : R), forall (b : R), R), forall (mul : forall (a : R), forall (b : R), R), forall (eI : R), forall (eJ : R), forall (a : R), forall (b : R), R :=
  fun R => fun add => fun mul => fun eI => fun eJ => fun a => fun b => add (mul eI a) (mul eJ b)

def RingCrtIntersectionPred.{u,v,w} :
  forall (R : Sort u), forall (RI : Sort v), forall (RJ : Sort w), forall (zeroI : RI), forall (zeroJ : RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (x : R), Prop :=
  fun R => fun RI => fun RJ => fun zeroI => fun zeroJ => fun modI => fun modJ => fun x => forall (Q : Prop), forall (mk : forall (left_kernel : @Eq.{v} RI (modI x) zeroI), forall (right_kernel : @Eq.{w} RJ (modJ x) zeroJ), Q), Q

def RingChineseRemainder.{p,u,v,w} :
  forall (R : Sort succ u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (zeroI : RI), forall (oneI : RI), forall (addI : forall (a : RI), forall (b : RI), RI), forall (negI : forall (a : RI), RI), forall (subI : forall (a : RI), forall (b : RI), RI), forall (mulI : forall (a : RI), forall (b : RI), RI), forall (RJ : Sort succ w), forall (zeroJ : RJ), forall (oneJ : RJ), forall (addJ : forall (a : RJ), forall (b : RJ), RJ), forall (negJ : forall (a : RJ), RJ), forall (subJ : forall (a : RJ), forall (b : RJ), RJ), forall (mulJ : forall (a : RJ), forall (b : RJ), RJ), forall (P : Sort succ p), forall (zeroP : P), forall (oneP : P), forall (addP : forall (a : P), forall (b : P), P), forall (negP : forall (a : P), P), forall (subP : forall (a : P), forall (b : P), P), forall (mulP : forall (a : P), forall (b : P), P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (ringR_args : @RingLawArgs.{succ u} R zeroR oneR addR negR subR mulR), forall (ringP_args : @RingLawArgs.{succ p} P zeroP oneP addP negP subP mulP), Prop :=
  fun R => fun zeroR => fun oneR => fun addR => fun negR => fun subR => fun mulR => fun RI => fun zeroI => fun oneI => fun addI => fun negI => fun subI => fun mulI => fun RJ => fun zeroJ => fun oneJ => fun addJ => fun negJ => fun subJ => fun mulJ => fun P => fun zeroP => fun oneP => fun addP => fun negP => fun subP => fun mulP => fun pair => fun fst => fun snd => fun modI => fun modJ => fun ringR_args => fun ringP_args => forall (Q : Prop), forall (mk : forall (pair_hom : @RingHomLawArgs.{succ u,succ p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (kernel_to_intersection : forall (x : R), forall (h : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), forall (intersection_to_kernel : forall (x : R), forall (h : @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), forall (first_iso_to_image : @RingFirstIso.{u,p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) ringR_args ringP_args pair_hom), forall (full_product_image : forall (y : P), @RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y), forall (quot_surj_product : forall (y : P), forall (S : Prop), forall (mk_surj : forall (q : @RingKerQuot.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (h : @Eq.{succ p} P (@RingKerQuotToS.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) q) y), S), S), Q), Q

theorem ring_crt_intersection_intro.{u,v,w} :
  forall (R : Sort u), forall (RI : Sort v), forall (RJ : Sort w), forall (zeroI : RI), forall (zeroJ : RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (x : R), forall (left_kernel : @Eq.{v} RI (modI x) zeroI), forall (right_kernel : @Eq.{w} RJ (modJ x) zeroJ), @RingCrtIntersectionPred.{u,v,w} R RI RJ zeroI zeroJ modI modJ x :=
  fun R => fun RI => fun RJ => fun zeroI => fun zeroJ => fun modI => fun modJ => fun x => fun left_kernel => fun right_kernel => fun (Q : Prop) => fun (mk : forall (left_kernel_arg : @Eq.{v} RI (modI x) zeroI), forall (right_kernel_arg : @Eq.{w} RJ (modJ x) zeroJ), Q) => mk left_kernel right_kernel

theorem ring_crt_intersection_left.{u,v,w} :
  forall (R : Sort u), forall (RI : Sort v), forall (RJ : Sort w), forall (zeroI : RI), forall (zeroJ : RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (x : R), forall (h : @RingCrtIntersectionPred.{u,v,w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{v} RI (modI x) zeroI :=
  fun R => fun RI => fun RJ => fun zeroI => fun zeroJ => fun modI => fun modJ => fun x => fun h => h (@Eq.{v} RI (modI x) zeroI) (fun (left_kernel_arg : @Eq.{v} RI (modI x) zeroI) => fun (right_kernel_arg : @Eq.{w} RJ (modJ x) zeroJ) => left_kernel_arg)

theorem ring_crt_intersection_right.{u,v,w} :
  forall (R : Sort u), forall (RI : Sort v), forall (RJ : Sort w), forall (zeroI : RI), forall (zeroJ : RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (x : R), forall (h : @RingCrtIntersectionPred.{u,v,w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{w} RJ (modJ x) zeroJ :=
  fun R => fun RI => fun RJ => fun zeroI => fun zeroJ => fun modI => fun modJ => fun x => fun h => h (@Eq.{w} RJ (modJ x) zeroJ) (fun (left_kernel_arg : @Eq.{v} RI (modI x) zeroI) => fun (right_kernel_arg : @Eq.{w} RJ (modJ x) zeroJ) => right_kernel_arg)

theorem ring_crt_pair_hom_laws.{p,u,v,w} :
  forall (R : Sort succ u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (zeroI : RI), forall (oneI : RI), forall (addI : forall (a : RI), forall (b : RI), RI), forall (negI : forall (a : RI), RI), forall (subI : forall (a : RI), forall (b : RI), RI), forall (mulI : forall (a : RI), forall (b : RI), RI), forall (RJ : Sort succ w), forall (zeroJ : RJ), forall (oneJ : RJ), forall (addJ : forall (a : RJ), forall (b : RJ), RJ), forall (negJ : forall (a : RJ), RJ), forall (subJ : forall (a : RJ), forall (b : RJ), RJ), forall (mulJ : forall (a : RJ), forall (b : RJ), RJ), forall (P : Sort succ p), forall (zeroP : P), forall (oneP : P), forall (addP : forall (a : P), forall (b : P), P), forall (negP : forall (a : P), P), forall (subP : forall (a : P), forall (b : P), P), forall (mulP : forall (a : P), forall (b : P), P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (homI_args : @RingHomLawArgs.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI), forall (homJ_args : @RingHomLawArgs.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (one_pair : @Eq.{succ p} P (pair oneI oneJ) oneP), forall (add_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (addI xI yI) (addJ xJ yJ)) (addP (pair xI xJ) (pair yI yJ))), forall (neg_pair : forall (xI : RI), forall (xJ : RJ), @Eq.{succ p} P (pair (negI xI) (negJ xJ)) (negP (pair xI xJ))), forall (mul_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (mulI xI yI) (mulJ xJ yJ)) (mulP (pair xI xJ) (pair yI yJ))), @RingHomLawArgs.{succ u,succ p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) :=
  fun R => fun zeroR => fun oneR => fun addR => fun negR => fun subR => fun mulR => fun RI => fun zeroI => fun oneI => fun addI => fun negI => fun subI => fun mulI => fun RJ => fun zeroJ => fun oneJ => fun addJ => fun negJ => fun subJ => fun mulJ => fun P => fun zeroP => fun oneP => fun addP => fun negP => fun subP => fun mulP => fun pair => fun modI => fun modJ => fun homI_args => fun homJ_args => fun zero_pair => fun one_pair => fun add_pair => fun neg_pair => fun mul_pair => fun (Q : Prop) => fun (mk : forall (hom_zero_law : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ zeroR) zeroP), forall (hom_one_law : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ oneR) oneP), forall (hom_add_law : forall (a : R), forall (b : R), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (addR a b)) (addP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b))), forall (hom_neg_law : forall (a : R), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (negR a)) (negP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a))), forall (hom_mul_law : forall (a : R), forall (b : R), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (mulR a b)) (mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b))), Q) => mk (@eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ zeroR) (pair zeroI zeroJ) zeroP (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI zeroR) zeroI (modJ zeroR) zeroJ (@ring_hom_zero.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args) (@ring_hom_zero.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args)) zero_pair) (@eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ oneR) (pair oneI oneJ) oneP (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI oneR) oneI (modJ oneR) oneJ (@ring_hom_one.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args) (@ring_hom_one.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args)) one_pair) (fun (a : R) => fun (b : R) => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (addR a b)) (pair (addI (modI a) (modI b)) (addJ (modJ a) (modJ b))) (addP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b)) (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (addR a b)) (addI (modI a) (modI b)) (modJ (addR a b)) (addJ (modJ a) (modJ b)) (@ring_hom_add.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args a b) (@ring_hom_add.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args a b)) (add_pair (modI a) (modI b) (modJ a) (modJ b))) (fun (a : R) => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (negR a)) (pair (negI (modI a)) (negJ (modJ a))) (negP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a)) (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (negR a)) (negI (modI a)) (modJ (negR a)) (negJ (modJ a)) (@ring_hom_neg.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args a) (@ring_hom_neg.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args a)) (neg_pair (modI a) (modJ a))) (fun (a : R) => fun (b : R) => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (mulR a b)) (pair (mulI (modI a) (modI b)) (mulJ (modJ a) (modJ b))) (mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b)) (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (mulR a b)) (mulI (modI a) (modI b)) (modJ (mulR a b)) (mulJ (modJ a) (modJ b)) (@ring_hom_mul.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args a b) (@ring_hom_mul.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args a b)) (mul_pair (modI a) (modI b) (modJ a) (modJ b)))

theorem ring_crt_kernel_to_intersection.{p,u,v,w} :
  forall (R : Sort succ u), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (zeroI : RI), forall (zeroJ : RJ), forall (zeroP : P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (fst_pair : forall (x : RI), forall (y : RJ), @Eq.{succ v} RI (fst (pair x y)) x), forall (snd_pair : forall (x : RI), forall (y : RJ), @Eq.{succ w} RJ (snd (pair x y)) y), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (x : R), forall (h : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x :=
  fun R => fun RI => fun RJ => fun P => fun zeroI => fun zeroJ => fun zeroP => fun pair => fun fst => fun snd => fun modI => fun modJ => fun fst_pair => fun snd_pair => fun zero_pair => fun x => fun h => @ring_crt_intersection_intro.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x (@eq_trans.{succ v} RI (modI x) (fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) zeroI (@eq_symm.{succ v} RI (fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (modI x) (fst_pair (modI x) (modJ x))) (@eq_trans.{succ v} RI (fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (fst zeroP) zeroI (@eq_congr_arg.{succ p,succ v} P RI fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP h) (@eq_trans.{succ v} RI (fst zeroP) (fst (pair zeroI zeroJ)) zeroI (@eq_symm.{succ v} RI (fst (pair zeroI zeroJ)) (fst zeroP) (@eq_congr_arg.{succ p,succ v} P RI fst (pair zeroI zeroJ) zeroP zero_pair)) (fst_pair zeroI zeroJ)))) (@eq_trans.{succ w} RJ (modJ x) (snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) zeroJ (@eq_symm.{succ w} RJ (snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (modJ x) (snd_pair (modI x) (modJ x))) (@eq_trans.{succ w} RJ (snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (snd zeroP) zeroJ (@eq_congr_arg.{succ p,succ w} P RJ snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP h) (@eq_trans.{succ w} RJ (snd zeroP) (snd (pair zeroI zeroJ)) zeroJ (@eq_symm.{succ w} RJ (snd (pair zeroI zeroJ)) (snd zeroP) (@eq_congr_arg.{succ p,succ w} P RJ snd (pair zeroI zeroJ) zeroP zero_pair)) (snd_pair zeroI zeroJ))))

theorem ring_crt_intersection_to_kernel.{p,u,v,w} :
  forall (R : Sort succ u), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (zeroI : RI), forall (zeroJ : RJ), forall (zeroP : P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (x : R), forall (left_kernel : @Eq.{succ v} RI (modI x) zeroI), forall (right_kernel : @Eq.{succ w} RJ (modJ x) zeroJ), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP :=
  fun R => fun RI => fun RJ => fun P => fun zeroI => fun zeroJ => fun zeroP => fun pair => fun modI => fun modJ => fun zero_pair => fun x => fun left_kernel => fun right_kernel => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) (pair zeroI zeroJ) zeroP (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI x) zeroI (modJ x) zeroJ left_kernel right_kernel) zero_pair

theorem ring_crt_pair_surjective.{p,u,v,w} :
  forall (R : Sort succ u), forall (addR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (eI : R), forall (eJ : R), forall (modI_surj : forall (y : RI), @RingImagePred.{succ u,succ v} R RI modI y), forall (modJ_surj : forall (y : RJ), @RingImagePred.{succ u,succ w} R RJ modJ y), forall (pair_eta : forall (z : P), @Eq.{succ p} P (pair (fst z) (snd z)) z), forall (combine_left : forall (a : R), forall (b : R), @Eq.{succ v} RI (modI (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modI a)), forall (combine_right : forall (a : R), forall (b : R), @Eq.{succ w} RJ (modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modJ b)), forall (y : P), @RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y :=
  fun R => fun addR => fun mulR => fun RI => fun RJ => fun P => fun pair => fun fst => fun snd => fun modI => fun modJ => fun eI => fun eJ => fun modI_surj => fun modJ_surj => fun pair_eta => fun combine_left => fun combine_right => fun y => modI_surj (fst y) (@RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y) (fun (a : R) => fun (ha : @Eq.{succ v} RI (modI a) (fst y)) => modJ_surj (snd y) (@RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y) (fun (b : R) => fun (hb : @Eq.{succ w} RJ (modJ b) (snd y)) => fun (Q : Prop) => fun (mk : forall (x : R), forall (h : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) y), Q) => mk (@RingCrtCombine.{succ u} R addR mulR eI eJ a b) (@eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (pair (modI a) (modJ b)) y (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modI a) (modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modJ b) (combine_left a b) (combine_right a b)) (@eq_trans.{succ p} P (pair (modI a) (modJ b)) (pair (fst y) (snd y)) y (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI a) (fst y) (modJ b) (snd y) ha hb) (pair_eta y)))))

theorem ring_chinese_remainder_theorem.{p,u,v,w} :
  forall (R : Sort succ u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (zeroI : RI), forall (oneI : RI), forall (addI : forall (a : RI), forall (b : RI), RI), forall (negI : forall (a : RI), RI), forall (subI : forall (a : RI), forall (b : RI), RI), forall (mulI : forall (a : RI), forall (b : RI), RI), forall (RJ : Sort succ w), forall (zeroJ : RJ), forall (oneJ : RJ), forall (addJ : forall (a : RJ), forall (b : RJ), RJ), forall (negJ : forall (a : RJ), RJ), forall (subJ : forall (a : RJ), forall (b : RJ), RJ), forall (mulJ : forall (a : RJ), forall (b : RJ), RJ), forall (P : Sort succ p), forall (zeroP : P), forall (oneP : P), forall (addP : forall (a : P), forall (b : P), P), forall (negP : forall (a : P), P), forall (subP : forall (a : P), forall (b : P), P), forall (mulP : forall (a : P), forall (b : P), P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (eI : R), forall (eJ : R), forall (ringR_args : @RingLawArgs.{succ u} R zeroR oneR addR negR subR mulR), forall (ringP_args : @RingLawArgs.{succ p} P zeroP oneP addP negP subP mulP), forall (homI_args : @RingHomLawArgs.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI), forall (homJ_args : @RingHomLawArgs.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (one_pair : @Eq.{succ p} P (pair oneI oneJ) oneP), forall (add_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (addI xI yI) (addJ xJ yJ)) (addP (pair xI xJ) (pair yI yJ))), forall (neg_pair : forall (xI : RI), forall (xJ : RJ), @Eq.{succ p} P (pair (negI xI) (negJ xJ)) (negP (pair xI xJ))), forall (mul_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (mulI xI yI) (mulJ xJ yJ)) (mulP (pair xI xJ) (pair yI yJ))), forall (fst_pair : forall (x : RI), forall (y : RJ), @Eq.{succ v} RI (fst (pair x y)) x), forall (snd_pair : forall (x : RI), forall (y : RJ), @Eq.{succ w} RJ (snd (pair x y)) y), forall (pair_eta : forall (z : P), @Eq.{succ p} P (pair (fst z) (snd z)) z), forall (modI_surj : forall (y : RI), @RingImagePred.{succ u,succ v} R RI modI y), forall (modJ_surj : forall (y : RJ), @RingImagePred.{succ u,succ w} R RJ modJ y), forall (combine_left : forall (a : R), forall (b : R), @Eq.{succ v} RI (modI (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modI a)), forall (combine_right : forall (a : R), forall (b : R), @Eq.{succ w} RJ (modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modJ b)), @RingChineseRemainder.{p,u,v,w} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI RJ zeroJ oneJ addJ negJ subJ mulJ P zeroP oneP addP negP subP mulP pair fst snd modI modJ ringR_args ringP_args :=
  fun R => fun zeroR => fun oneR => fun addR => fun negR => fun subR => fun mulR => fun RI => fun zeroI => fun oneI => fun addI => fun negI => fun subI => fun mulI => fun RJ => fun zeroJ => fun oneJ => fun addJ => fun negJ => fun subJ => fun mulJ => fun P => fun zeroP => fun oneP => fun addP => fun negP => fun subP => fun mulP => fun pair => fun fst => fun snd => fun modI => fun modJ => fun eI => fun eJ => fun ringR_args => fun ringP_args => fun homI_args => fun homJ_args => fun zero_pair => fun one_pair => fun add_pair => fun neg_pair => fun mul_pair => fun fst_pair => fun snd_pair => fun pair_eta => fun modI_surj => fun modJ_surj => fun combine_left => fun combine_right => fun (Q : Prop) => fun (mk : forall (pair_hom : @RingHomLawArgs.{succ u,succ p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (kernel_to_intersection : forall (x : R), forall (h : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), forall (intersection_to_kernel : forall (x : R), forall (h : @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), forall (first_iso_to_image : @RingFirstIso.{u,p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) ringR_args ringP_args pair_hom), forall (full_product_image : forall (y : P), @RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y), forall (quot_surj_product : forall (y : P), forall (S : Prop), forall (mk_surj : forall (q : @RingKerQuot.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (h : @Eq.{succ p} P (@RingKerQuotToS.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) q) y), S), S), Q) => mk (@ring_crt_pair_hom_laws.{p,u,v,w} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI RJ zeroJ oneJ addJ negJ subJ mulJ P zeroP oneP addP negP subP mulP pair modI modJ homI_args homJ_args zero_pair one_pair add_pair neg_pair mul_pair) (@ring_crt_kernel_to_intersection.{p,u,v,w} R RI RJ P zeroI zeroJ zeroP pair fst snd modI modJ fst_pair snd_pair zero_pair) (fun (x : R) => fun (h : @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x) => h (@Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP) (fun (left_kernel : @Eq.{succ v} RI (modI x) zeroI) => fun (right_kernel : @Eq.{succ w} RJ (modJ x) zeroJ) => @ring_crt_intersection_to_kernel.{p,u,v,w} R RI RJ P zeroI zeroJ zeroP pair modI modJ zero_pair x left_kernel right_kernel)) (@ring_first_isomorphism_to_image.{u,p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) ringR_args ringP_args (@ring_crt_pair_hom_laws.{p,u,v,w} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI RJ zeroJ oneJ addJ negJ subJ mulJ P zeroP oneP addP negP subP mulP pair modI modJ homI_args homJ_args zero_pair one_pair add_pair neg_pair mul_pair)) (@ring_crt_pair_surjective.{p,u,v,w} R addR mulR RI RJ P pair fst snd modI modJ eI eJ modI_surj modJ_surj pair_eta combine_left combine_right) (fun (y : P) => fun (S : Prop) => fun (mk_surj : forall (q : @RingKerQuot.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (h : @Eq.{succ p} P (@RingKerQuotToS.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) q) y), S) => @ring_first_iso_phi_surj_image.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y (@ring_crt_pair_surjective.{p,u,v,w} R addR mulR RI RJ P pair fst snd modI modJ eI eJ modI_surj modJ_surj pair_eta combine_left combine_right y) S mk_surj)