-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu (goal)
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)
F : Finset (Discrete (↑M : Type v))
⊢ Eq (α :=
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
        ∐ fun (x : (↑M : Type v)) ↦ G)
        (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F :
          Quiver.Hom.{v, u} (V := C) (Functor.obj (liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G)) F)
            (Functor.obj (Functor.obj (Functor.const (Finset (Discrete (↑M : Type v)))) (∐ fun (x : (↑M : Type v)) ↦ G))
              F))
        (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) ⟶
      B)
    (CategoryStruct.comp (Y := kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A))
        (pullback.snd (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F)
            (kernel.ι (d g)) :
          pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
              kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
              ∐ fun (x : (↑M : Type v)) ↦ G)
              (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F :
                Quiver.Hom.{v, u} (V := C)
                  (Functor.obj (liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G)) F)
                  (Functor.obj
                    (Functor.obj (Functor.const (Finset (Discrete (↑M : Type v)))) (∐ fun (x : (↑M : Type v)) ↦ G)) F))
              (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) ⟶
            kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A))
        (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) :
      pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
          kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
          ∐ fun (x : (↑M : Type v)) ↦ G)
          (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone fun (x : (↑M : Type v)) ↦ G)) F :
            Quiver.Hom.{v, u} (V := C) (Functor.obj (liftToFinsetObj (Discrete.functor fun (x : (↑M : Type v)) ↦ G)) F)
              (Functor.obj
                (Functor.obj (Functor.const (Finset (Discrete (↑M : Type v)))) (∐ fun (x : (↑M : Type v)) ↦ G)) F))
          (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) ⟶
        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)
have rw : Eq (α :=
  pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
      kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
      ∐ fun (x : (↑M : Type v)) ↦ G)
      (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
        Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ 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) ⟶
    B)
  (pullback.fst
        (∑ a ∈ F.attach,
          Sigma.π (fun (a : ↥F) ↦ G) a ≫
            Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as)
        (kernel.ι (d g)) ≫
      CategoryStruct.comp (Y := ∐ fun (x : (↑M : Type v)) ↦ G)
        (∑ a ∈ F.attach,
            Sigma.π (fun (a : ↥F) ↦ G) a ≫
              Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
          Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ fun (x : (↑M : Type v)) ↦ G))
        (d f : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ B) :
    pullback (X := ∐ fun (x : ↥F) ↦ G) (Y :=
        kernel (X := ∐ fun (x : (↑M : Type v)) ↦ G) (d g : (∐ fun (x : (↑M : Type v)) ↦ G) ⟶ A)) (Z :=
        ∐ fun (x : (↑M : Type v)) ↦ G)
        (∑ a ∈ F.attach,
            Sigma.π (fun (a : ↥F) ↦ G) a ≫
              Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
          Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ 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) ⟶
      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)
        (∑ a ∈ F.attach,
            Sigma.π (fun (a : ↥F) ↦ G) a ≫
              Sigma.ι.{v, v, u} (C := C) (fun (x : (↑M : Type v)) ↦ G) (↑a : Discrete (↑M : Type v)).as :
          Quiver.Hom.{v, u} (V := C) (∐ fun (a : ↥F) ↦ G) (∐ 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) ⟶
      B)
Tactic: rw [finiteSubcoproductsCocone_ι_app_eq_sum, ← pullback.condition_assoc]