-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator.{v, u} G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
refine :
  ∀ (F : Finset (Discrete (↑M : Type v))),
    Eq (α :=
      pullback (X := Functor.obj (liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G)) F) (Y :=
          kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
          Functor.obj
            (Functor.obj (Functor.const (Finset (Discrete (↑M : Type v))))
              (Cocone.pt.{v, v, v, u} (J := Finset (Discrete (↑M : Type v))) (F :=
                liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G))
                (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)))
            F)
          (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F) (kernel.ι (d g)) ⟶
        B)
      (pullback.snd (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F)
            (kernel.ι (d g)) ≫
          CategoryStruct.comp (Y :=
            Cocone.pt.{v, v, v, u} (J := Finset (Discrete (↑M : Type v))) (F :=
              liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G))
              (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G))
            (kernel.ι (d g) :
              kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
                ∐ fun (x : (↑M : Type v)) ↦ G)
            (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B) :
        pullback (X := Functor.obj (liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G)) F) (Y :=
            kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
            Functor.obj
              (Functor.obj (Functor.const (Finset (Discrete (↑M : Type v))))
                (Cocone.pt.{v, v, v, u} (J := Finset (Discrete (↑M : Type v))) (F :=
                  liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G))
                  (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)))
              F)
            (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F) (kernel.ι (d g)) ⟶
          B)
      (0 :
        pullback (X := Functor.obj (liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G)) F) (Y :=
            kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
            Functor.obj
              (Functor.obj (Functor.const (Finset (Discrete (↑M : Type v))))
                (Cocone.pt.{v, v, v, u} (J := Finset (Discrete (↑M : Type v))) (F :=
                  liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G))
                  (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)))
              F)
            (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F) (kernel.ι (d g)) ⟶
          B)
⊢ Eq (α := kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶ B)
    (CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
        (kernel.ι (d g) :
          kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶
            ∐ fun (x : (↑M : Type v)) ↦ G)
        (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B) :
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶ B)
    (0 : kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A) ⟶ B)

Tactic:
refine (isColimitFiniteSubproductsCocone (fun (_ : M) => G)).pullback_zero_ext (fun F => ?_)

Premises used: CategoryTheory.Limits.CoproductsFromFiniteFiltered.isColimitFiniteSubproductsCocone, CategoryTheory.Limits.IsColimit.pullback_zero_ext