-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
theorem exists_epi (X : D) : ∃ f : generator F ⟶ F.obj X, Epi f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
⊢ ∃ f, Epi f

Tactic:
refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
⊢ Epi
    (Sigma.desc
        (Pi.single X
          (𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C))) ≫
      Sigma.desc fun f => f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
⊢ ∃ f, Epi 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⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
h : Epi (Sigma.desc fun f => f)
⊢ Epi
    (Sigma.desc
        (Pi.single X
          (𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C))) ≫
      Sigma.desc fun f => f)

Tactic:
suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
h : Epi (Sigma.desc fun f => f)
⊢ Epi
    (Sigma.desc
      (Pi.single X
        (𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C))))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
⊢ Epi
    (Sigma.desc
        (Pi.single X
          (𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C))) ≫
      Sigma.desc fun f => f)

Tactic:
have h := (isSeparator_iff_epi (projectiveSeparator C)).1
  isSeparator_projectiveSeparator (F.obj X)

Result:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
h : Epi (Sigma.desc fun f => f)
⊢ Epi
    (Sigma.desc
        (Pi.single X
          (𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C))) ≫
      Sigma.desc fun f => f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
h : Epi (Sigma.desc fun f => f)
⊢ Epi
    (Sigma.desc
      (Pi.single X
        (𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C))))

Tactic:
exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
X : D
h : Epi (Sigma.desc fun f => f)
⊢ Sigma.ι
        (fun X => ∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C)
        X ≫
      Sigma.desc
        (Pi.single X
          (𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C))) =
    𝟙 (∐ fun x => CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.projectiveSeparator C)

Tactic:
simp

Result:
no goals