case mp
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D

case mpr
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughProjectives C ↔ EnoughProjectives D
constructor
case mp.presentation.val
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X

case mpr.presentation.val
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X
case mp
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D

case mpr
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C
all_goals intro H; constructor; intro X; constructor
case mpr
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ EnoughProjectives C
case mpr
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C
intro H
case mpr.presentation
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ ∀ (X : C), Nonempty (ProjectivePresentation X)
case mpr
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ EnoughProjectives C
constructor
case mpr.presentation
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ Nonempty (ProjectivePresentation X)
case mpr.presentation
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ ∀ (X : C), Nonempty (ProjectivePresentation X)
intro X
case mpr.presentation.val
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X
case mpr.presentation
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ Nonempty (ProjectivePresentation X)
constructor
no goals
case mp.presentation.val
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X
exact F.symm.projectivePresentationOfMapProjectivePresentation _
  (Nonempty.some (H.presentation (F.inverse.obj X)))
no goals
case mpr.presentation.val
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X
exact F.projectivePresentationOfMapProjectivePresentation X
  (Nonempty.some (H.presentation (F.functor.obj X)))