-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
x y z : (j : J) × F.obj j
h_1 : FilteredColimit.Rel F x y
h_2 : FilteredColimit.Rel F y z
k : J
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj x.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
    ((hom (FC := TypeCat.Fun) (F.map g) : (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k))
k' : J
f' : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k'
g' : z.fst (β := fun (j : J) ↦ F.obj j) ⟶ k'
h' :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj k'))
    ((hom (FC := TypeCat.Fun) (F.map f') :
          (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k'))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k'))
    ((hom (FC := TypeCat.Fun) (F.map g') :
          (a : (fun (X : Type u) ↦ X) (F.obj z.fst)) → (fun (X : Type u) ↦ X) (F.obj k'))
        (z.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj k'))
l : J
fl : k ⟶ l
gl : k' ⟶ l
h_3 : True
m : J
n : l ⟶ m
hn : (g ≫ fl) ≫ n = (f' ≫ gl) ≫ n
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj m))
    ((hom (FC := TypeCat.Fun) (F.map (gl ≫ n)) :
          (a : (fun (X : Type u) ↦ X) (F.obj k')) → (fun (X : Type u) ↦ X) (F.obj m))
        ((hom (FC := TypeCat.Fun) (F.map f') :
              (a : (fun (X : Type u) ↦ X) (F.obj y.fst)) → (fun (X : Type u) ↦ X) (F.obj k'))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type u) ↦ X) (F.obj k')) :
      (fun (X : Type u) ↦ X) (F.obj m))
    ((hom (FC := TypeCat.Fun) (F.map (gl ≫ n)) :
          (a : (fun (X : Type u) ↦ X) (F.obj k')) → (fun (X : Type u) ↦ X) (F.obj m))
        ((hom (FC := TypeCat.Fun) (F.map g') :
              (a : (fun (X : Type u) ↦ X) (F.obj z.fst)) → (fun (X : Type u) ↦ X) (F.obj k'))
            (z.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type u) ↦ X) (F.obj k')) :
      (fun (X : Type u) ↦ X) (F.obj m))
have rw : Eq (α := (fun (X : Type u) ↦ X) (F.obj m))
  ((hom (FC := TypeCat.Fun) (F.map (gl ≫ n)) :
        (a : (fun (X : Type u) ↦ X) (F.obj k')) → (fun (X : Type u) ↦ X) (F.obj m))
      ((hom (FC := TypeCat.Fun) (F.map g') :
            (a : (fun (X : Type u) ↦ X) (F.obj z.fst)) → (fun (X : Type u) ↦ X) (F.obj k'))
          (z.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type u) ↦ X) (F.obj k')) :
    (fun (X : Type u) ↦ X) (F.obj m))
  ((hom (FC := TypeCat.Fun) (F.map (gl ≫ n)) :
        (a : (fun (X : Type u) ↦ X) (F.obj k')) → (fun (X : Type u) ↦ X) (F.obj m))
      ((hom (FC := TypeCat.Fun) (F.map g') :
            (a : (fun (X : Type u) ↦ X) (F.obj z.fst)) → (fun (X : Type u) ↦ X) (F.obj k'))
          (z.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type u) ↦ X) (F.obj k')) :
    (fun (X : Type u) ↦ X) (F.obj m))
Tactic: rw [h']