-- Lean 4 proof step from Mathlib.Algebra.Colimit.Ring (goal)
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 ι
⊢ 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')
have 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') sorry)
                (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)) sorry))
              (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')
Tactic: ext