-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
h :
  ∀ (g : (i : J) → (↑(X.obj { as := i }) : Type u)) (j : J),
    Eq (α := (↑(Y.obj { as := j }) : Type u))
      (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
          (fun (i : J) ↦
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                  AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
              (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
          g j :
        (↑(Y.obj { as := j }) : Type u))
      (((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) (X := AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) (Y :=
                AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
                (CategoryStruct.comp (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j })
                    (limit.lift (Discrete.functor fun (j : J) ↦ X.obj { as := j })
                        { pt := AddCommGrpCat.of ((j : J) → (↑(X.obj { as := j }) : Type u)),
                          π :=
                            Discrete.natTrans fun (j : Discrete J) ↦
                              AddCommGrpCat.ofHom
                                (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(X.obj { as := j }) : Type u)) j.as) } :
                      Cone.pt (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ X.obj { as := j : Discrete J })
                          { pt := AddCommGrpCat.of ((j : J) → (↑(X.obj { as := j : Discrete J }) : Type u)),
                            π :=
                              Discrete.natTrans fun (j : Discrete J) ↦
                                AddCommGrpCat.ofHom
                                  (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(X.obj { as := j : Discrete J }) : Type u))
                                    j.as) :
                            Cone (J := Discrete J) (C := AddCommGrpCat)
                              (Discrete.functor fun (j : J) ↦ X.obj { as := j : Discrete J }) } ⟶
                        limit (J := Discrete J) (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
                    (CategoryStruct.comp (Y := limit Y) (limit.lift Y ((Cone.postcompose f).obj (Pi.cone X)))
                        (CategoryStruct.comp (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j })
                          (IsLimit.lift (productIsProduct' Y) (getLimitCone Y).cone)
                          (AddCommGrpCat.ofHom
                            {
                              toFun :=
                                fun
                                  (x :
                                    (↑(LimitCone.cone
                                            (getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))).1 :
                                      Type u))
                                  (j : J) ↦
                                (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
                                      (fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                                      AddCommGrpCat.carrier _ _
                                      (Cone.pt (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ Y.obj { as := j })
                                        (LimitCone.cone
                                          (getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))))
                                      _
                                      (NatTrans.app
                                        (Cone.π
                                          (LimitCone.cone
                                            (getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))))
                                        { as := j }) :
                                    (a :
                                        (↑(getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j })).cone.pt :
                                          Type u)) →
                                      (↑(Y.obj { as := j }) : Type u))
                                  x,
                              map_zero' := ⋯, map_add' := ⋯ })) :
                      (∏ᶜ fun (j : J) ↦ X.obj { as := j }) ⟶
                        AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i : Discrete J }) : Type u))) :
                  AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i : Discrete J }) : Type u)) ⟶
                    AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) :
              (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u) →+
                (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u)) :
            (a : (i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
          g j :
        (↑(Y.obj { as := j }) : Type u))
⊢ Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) (Y :=
            AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
            (CategoryStruct.comp (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j })
                (limit.lift (Discrete.functor fun (j : J) ↦ X.obj { as := j })
                    { pt := AddCommGrpCat.of ((j : J) → (↑(X.obj { as := j }) : Type u)),
                      π :=
                        Discrete.natTrans fun (j : Discrete J) ↦
                          AddCommGrpCat.ofHom
                            (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(X.obj { as := j }) : Type u)) j.as) } :
                  Cone.pt (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ X.obj { as := j : Discrete J })
                      { pt := AddCommGrpCat.of ((j : J) → (↑(X.obj { as := j : Discrete J }) : Type u)),
                        π :=
                          Discrete.natTrans fun (j : Discrete J) ↦
                            AddCommGrpCat.ofHom
                              (Pi.evalAddMonoidHom (fun (j : J) ↦ (↑(X.obj { as := j : Discrete J }) : Type u)) j.as) :
                        Cone (J := Discrete J) (C := AddCommGrpCat)
                          (Discrete.functor fun (j : J) ↦ X.obj { as := j : Discrete J }) } ⟶
                    limit (J := Discrete J) (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
                (CategoryStruct.comp (Y := limit Y) (limit.lift Y ((Cone.postcompose f).obj (Pi.cone X)))
                    (CategoryStruct.comp (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j })
                      (IsLimit.lift (productIsProduct' Y) (getLimitCone Y).cone)
                      (AddCommGrpCat.ofHom
                        {
                          toFun :=
                            fun
                              (x :
                                (↑(LimitCone.cone (getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))).1 :
                                  Type u))
                              (j : J) ↦
                            (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
                                  (fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
                                  AddCommGrpCat.carrier _ _
                                  (Cone.pt (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ Y.obj { as := j })
                                    (LimitCone.cone (getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))))
                                  _
                                  (NatTrans.app
                                    (Cone.π
                                      (LimitCone.cone
                                        (getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))))
                                    { as := j }) :
                                (a :
                                    (↑(getLimitCone (Discrete.functor fun (j : J) ↦ Y.obj { as := j })).cone.pt :
                                      Type u)) →
                                  (↑(Y.obj { as := j }) : Type u))
                              x,
                          map_zero' := ⋯, map_add' := ⋯ })) :
                  (∏ᶜ fun (j : J) ↦ X.obj { as := j }) ⟶
                    AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i : Discrete J }) : Type u))) :
              AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i : Discrete J }) : Type u)) ⟶
                AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) :
          (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u) →+
            (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u)) :
      (a : (i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))

Tactic:
ext g j