-- 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 (α := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      ((RingHom.comp (β := DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
              (@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)) _
                (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)) ⋯)
                (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') ⋯))
              (of G (fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) i) :
            (a : G i) → DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
          x :
        DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
      ((RingHom.comp (RingHom.id (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)) i) :
            (a : G i) → DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
          x :
        DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
⊢ Eq (α :=
    (DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)) →+*
      DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2))
    (@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)) _
      (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)) ⋯)
      (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') ⋯))
    (RingHom.id (DirectLimit G fun (x1 x2 : ι) (x3 : x1 ≤ x2) ↦ (⇑(f' x1 x2 x3) : (a : G x1) → G x2)))

Tactic:
ext