-- Mathlib/CategoryTheory/Abelian/Yoneda.lean
theorem preadditiveCoyonedaObj_map_surjective {G : C} [Projective G] (hG : IsSeparator G) {X : C}
    (p : G ⟶ X) [Epi p] {Y : C} :
    Function.Surjective ((preadditiveCoyonedaObj G).map : (X ⟶ Y) → _)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Epi (AddCommGrp.ofHom (preadditiveCoyonedaObj G).mapAddHom)

Tactic:
apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))

Result:
case hR₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ (cm.op.map (preadditiveYoneda.obj Y)).Exact

case hR₂'
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Mono (cm.op.map ((preadditiveCoyonedaObj G).op ⋙ preadditiveYoneda.obj ((preadditiveCoyonedaObj G).obj Y))).f

case h₀
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Epi (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)).τ₂

case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Mono (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)).τ₃

Proof state:
case h₀
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Function.Surjective φ.map

Tactic:
exact fun f => ⟨f (𝟙 G), by aesop_cat⟩

Result:
no goals

Proof state:
case hR₂'
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Mono (cm.op.map ((preadditiveCoyonedaObj G).op ⋙ preadditiveYoneda.obj ((preadditiveCoyonedaObj G).obj Y))).f

Tactic:
simp only [ShortComplex.map_f]

Result:
case hR₂'
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Mono (((preadditiveCoyonedaObj G).op ⋙ preadditiveYoneda.obj ((preadditiveCoyonedaObj G).obj Y)).map cm.op.f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
⊢ Epi (AddCommGrp.ofHom (preadditiveCoyonedaObj G).mapAddHom)

Tactic:
have exact : cm.Exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel _)

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
⊢ Epi (AddCommGrp.ofHom (preadditiveCoyonedaObj G).mapAddHom)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
⊢ Mono cm.op.f

Tactic:
dsimp [cm]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := ShortComplex.mk (kernel.ι p) p ⋯
exact : cm.Exact
⊢ Mono p.op