-- Module: Mathlib.Algebra.Colimit.Ring
Goal:
ι : Type u_1
inst : Preorder ι
G : ι → Type u_2
inst_1 : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst_2 : CommRing P
g : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g j : (a : G j) → P) (f i j hij x) : P) ((g i : (a : G i) → P) x : P)
f' : (i j : ι) → i ≤ j → G i →+* G j
inst_3 : DirectedSystem G fun (i j : ι) (h : i ≤ j) ↦ (⇑(f' i j h) : (a : G i) → G j)
inst_4 : IsDirectedOrder ι
inst_5 : Nonempty ι
h :
  ∀ (i : ι) (x : G i),
    Eq (α := _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
      (((@RingHom.comp _ (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') _ _
                (instNonAssocSemiringOfRingHomClass (G := G) (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j)) _
                (RingHom.comp (β := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
                  (lift G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
                    (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
                    (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') ⋯)
                  (Ring.lift G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'
                    (DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
                    (of G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) ⋯))
                (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f' i) :
              G i →+* _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') :
            (a : G i) → _root_.DirectLimit G f')
          x :
        _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
      (((RingHom.comp (RingHom.id (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'))
                (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f' i) :
              G i →+* _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') :
            (a : G i) → _root_.DirectLimit G f')
          x :
        _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
⊢ Eq (α :=
    _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f' →+*
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    (RingHom.comp (β := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
        (lift G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
          (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
          (Ring.of G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') ⋯)
        (Ring.lift G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f'
          (DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
          (of G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) ⋯) :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f' →+*
        _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')
    (RingHom.id (_root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f') :
      _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f' →+*
        _root_.DirectLimit G (T := fun (i j : ι) (h : i ≤ j) ↦ G i →+* G j) f')

Tactic:
ext