-- Module: Mathlib.Algebra.Category.Grp.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ GrpCat
x y : (j : J) × (↑(F.obj j) : Type (max u v))
h :
  Types.FilteredColimit.Rel
    (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
    x y
h₁ :
  ∀ (k : J)
    (f :
      x.fst (β := fun (j : J) ↦
          (F ⋙
                forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).obj
            j) ⟶
        k)
    (g :
      y.fst (β := fun (j : J) ↦
          (F ⋙
                forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).obj
            j) ⟶
        k)
    (hfg :
      Eq (α :=
        (fun (X : Type (max u v)) ↦ X)
          ((F ⋙
                forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).obj
            k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                        (CC := carrier)).map
                  f) :
              (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget GrpCat).obj x.fst)) →
                (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget GrpCat).obj k))
            (x.snd (β := fun (j : J) ↦
              (F ⋙
                    forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).obj
                j)) :
          (fun (X : Type (max u v)) ↦ X)
            ((F ⋙
                  forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).obj
              k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((F ⋙
                      forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                        (CC := carrier)).map
                  g) :
              (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget GrpCat).obj y.fst)) →
                (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget GrpCat).obj k))
            (y.snd (β := fun (j : J) ↦
              (F ⋙
                    forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).obj
                j)) :
          (fun (X : Type (max u v)) ↦ X)
            ((F ⋙
                  forget GrpCat (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑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))))
            (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))))
            (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))⁻¹) ⟶
        k),
      Eq (α := (↑(F.obj k) : Type (max u v)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj ⟨x.fst, 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))))
                (x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))⁻¹)) :
          (↑(F.obj k) : Type (max u v)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier) (F.map g) :
              (a : (↑(F.obj ⟨y.fst, 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))))
                (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))⁻¹)) :
          (↑(F.obj k) : Type (max u v)))
⊢ ∃ (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))))
          (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))))
          (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))⁻¹) ⟶
      k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj ⟨x.fst, 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))))
              (x.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))))⁻¹)) :
        (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map g) :
            (a : (↑(F.obj ⟨y.fst, 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))))
              (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