-- Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
Goal:
C : Type u
inst : Category.{v, u} C
D : Type v
inst_1 : SmallCategory D
F : Functor.{v, v, v, u} D Cᵒᵖ
inst_2 : Abelian.{v, u} C
inst_3 : IsGrothendieckAbelian.{v, v, u} C
X : D
refine :
  Epi.{v, u} (C := Cᵒᵖ) (X := generator F) (Y := F.obj X)
    (CategoryStruct.comp (Y := ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
      (Sigma.desc
        (Pi.single (M := fun (b : D) ↦
          Quiver.Hom.{v, u} (V := Cᵒᵖ)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
          X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))))
      (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f))
refine₁ :
  ∀
    (h :
      Epi.{v, u} (C := Cᵒᵖ) (X := ∐ fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
        (Y := F.obj X) (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f)),
    Epi.{v, u} (C := Cᵒᵖ) (X := generator F) (Y := F.obj X)
      (CategoryStruct.comp (Y := ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
        (Sigma.desc
          (Pi.single (M := fun (b : D) ↦
            Quiver.Hom.{v, u} (V := Cᵒᵖ)
              (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
              (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
            X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))))
        (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f))
refine₂ :
  ∀
    (h :
      Epi.{v, u} (C := Cᵒᵖ) (X := ∐ fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
        (Y := F.obj X) (Sigma.desc fun (f : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ f)),
    Epi.{v, u} (C := Cᵒᵖ) (X :=
      ∐ fun (X : D) ↦ ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C) (Y :=
      ∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C)
      (Sigma.desc
        (Pi.single (M := fun (b : D) ↦
          Quiver.Hom.{v, u} (V := Cᵒᵖ)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj b) ↦ projectiveSeparator.{v, u} C)
            (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))
          X (𝟙 (∐ fun (x : projectiveSeparator.{v, u} C ⟶ F.obj X) ↦ projectiveSeparator.{v, u} C))))
⊢ ∃ (f : generator F ⟶ F.obj X), Epi.{v, u} (C := Cᵒᵖ) (X := generator F) (Y := F.obj X) f

Tactic:
classical
  refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
  have h := (isSeparator_iff_epi (projectiveSeparator C)).1
    isSeparator_projectiveSeparator (F.obj X)
  suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
  exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩

Premises used: CategoryTheory.Limits.Sigma.ι, _private.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator, CategoryTheory.SplitEpi.mk, CategoryTheory.Limits.sigmaObj, CategoryTheory.SplitEpi.epi