∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} {G'' : ι → Type u_5} [inst_3 : (i : ι) → CommRing (G'' i)]
  {f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j} (g₁ : (i : ι) → G i →+* G' i) (g₂ : (i : ι) → G' i →+* G'' i)
  (hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
  (hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)),
  (Ring.DirectLimit.map g₂ hg₂).comp (Ring.DirectLimit.map g₁ hg₁) =
    Ring.DirectLimit.map (fun i => (g₂ i).comp (g₁ i)) ⋯