-- 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_1 : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst_2 : CommRing P
g_1 : (i : ι) → RingHom.{u_2, u_3} (G i) P
Hg :
  ∀ (i j : ι) (hij : i ≤ j) (x : G i),
    Eq.{u_3 + 1} (α := P) ((g_1 j : (a : G j) → P) (f_1 i j hij x) : P) ((g_1 i : (a : G i) → P) x : P)
f'_1 f : (i j : ι) → i ≤ j → G i →+* G j
G' : ι → Type u_4
inst_3 : (i : ι) → CommRing (G' i)
f' : (i j : ι) → i ≤ j → G' i →+* G' j
G'' : ι → Type u_5
inst_4 : (i : ι) → CommRing (G'' i)
f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j
g_2 : (i : ι) → RingHom.{u_2, u_4} (G i) (G' i)
hg : ∀ (i j : ι) (h : i ≤ j), (g_2 j).comp (f i j h) = (f' i j h).comp (g_2 i)
i j : ι
h : i ≤ j
g : G i
eq1 :
  Eq.{u_4 + 1} (α := G' j) ((g_2 j : (a : G j) → G' j) ((f i j h : (a : G i) → G j) g) : G' j)
    ((f' i j h : (a : G' i) → G' j) ((g_2 i : (a : G i) → G' i) g : G' i) : G' j)
rw :
  Eq (α := DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) j :
          (a : G' j) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((f' i j h : (a : G' i) → G' j) ((g_2 i : (a : G i) → G' i) g : G' i)) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) i :
          (a : G' i) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((g_2 i : (a : G i) → G' i) g) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
⊢ Eq (α := DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) j :
          (a : G' j) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((g_2 j : (a : G j) → G' j) ((f i j h : (a : G i) → G j) g)) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
    ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) i :
          (a : G' i) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
        ((g_2 i : (a : G i) → G' i) g) :
      DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
have rw₁ : Eq (α := DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
  ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) i :
        (a : G' i) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
      ((g_2 i : (a : G i) → G' i) g) :
    DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
  ((of G' (fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1)) i :
        (a : G' i) → DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
      ((g_2 i : (a : G i) → G' i) g) :
    DirectLimit G' fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f' x x_1 h) : (a : G' x) → G' x_1))
Tactic: rw [eq1, of_f]