case intro
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ ∃ f', f' ≫ g = f
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f
rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩
case intro
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E✝) ≫ g = f
case intro
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ ∃ f', f' ≫ g = f
use F.map f' ≫ adj.counit.app _
case intro
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X✝ = f
case intro
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E✝) ≫ g = f
rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']
no goals
case intro
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X✝ = f
simp