-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.FilteredColimits (goal)
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : SmallCategory J
inst_2 : IsFiltered J
F : J ⥤ ModuleCat R
r : R
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  Types.FilteredColimit.Rel
    (F ⋙
      forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v)))
        (CC := carrier))
    x y
⊢ ∃ (k : J) (f :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
          (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))) ⟶
      k)
    (g :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
          (r • y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))) ⟶
      k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj ⟨x.fst, r • x.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
              (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
        (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map g) :
            (a : (↑(F.obj ⟨y.fst, r • y.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
              (r • y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
        (↑(F.obj k) : Type (max u v)))
have h₁ : ∀ (k : J)
  (f :
    x.fst (β := fun (j : J) ↦
        (F ⋙
              forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
          j) ⟶
      k)
  (g :
    y.fst (β := fun (j : J) ↦
        (F ⋙
              forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
          j) ⟶
      k)
  (hfg :
    Eq (α :=
      (fun (X : Type (max u v)) ↦ X)
        ((F ⋙
              forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
          k))
      ((hom (FC := TypeCat.Fun)
              ((F ⋙
                    forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                      (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).map
                f) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj x.fst)) →
              (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj k))
          (x.snd (β := fun (j : J) ↦
            (F ⋙
                  forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
              j)) :
        (fun (X : Type (max u v)) ↦ X)
          ((F ⋙
                forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
            k))
      ((hom (FC := TypeCat.Fun)
              ((F ⋙
                    forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                      (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).map
                g) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj y.fst)) →
              (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget (ModuleCat R)).obj k))
          (y.snd (β := fun (j : J) ↦
            (F ⋙
                  forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
              j)) :
        (fun (X : Type (max u v)) ↦ X)
          ((F ⋙
                forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)).obj
            k))),
  ∃ (k : J) (f :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
          (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))) ⟶
      k)
    (g :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
          (r • y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))) ⟶
      k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map f) :
            (a : (↑(F.obj ⟨x.fst, r • x.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (x.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
              (r • x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
        (↑(F.obj k) : Type (max u v)))
      ((hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max u v)) →ₗ[R] (↑x2 : Type (max u v))) (CC := carrier)
              (F.map g) :
            (a : (↑(F.obj ⟨y.fst, r • y.snd⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (y.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))
              (r • y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))))) :
        (↑(F.obj k) : Type (max u v)))
Tactic: obtain ⟨k, f, g, hfg⟩ := h
Cleared hypotheses: h