-- 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 (α :=
    (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)))
have 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)) sorry)
              (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))
            (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))
Tactic: ext