-- 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))
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))
h :
  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)))
        (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)))
        (y.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))) :
      (↑(F.obj k) : Type (max u v)))
⊢ 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:
rw [map_inv, map_inv, inv_inj]

Premises used: map_inv, inv_inj