-- Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean
theorem enoughProjectives_iff (F : C ≌ D) : EnoughProjectives C ↔ EnoughProjectives D

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C

Tactic:
intro H

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
⊢ EnoughProjectives C

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
⊢ EnoughProjectives C

Tactic:
constructor

Result:
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
⊢ ∀ (X : C), Nonempty (ProjectivePresentation X)

Proof state:
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
⊢ ∀ (X : C), Nonempty (ProjectivePresentation X)

Tactic:
intro X

Result:
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
X : C
⊢ Nonempty (ProjectivePresentation X)

Proof state:
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
X : C
⊢ Nonempty (ProjectivePresentation X)

Tactic:
constructor

Result:
case mpr.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives C ↔ EnoughProjectives D

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C

Proof state:
case mpr.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X

Tactic:
exact F.projectivePresentationOfMapProjectivePresentation X
  (Nonempty.some (H.presentation (F.functor.obj X)))

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C

Tactic:
all_goals intro H; constructor; intro X; constructor

Result:
case mp.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X

case mpr.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X

Proof state:
case mp.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X

Tactic:
exact F.symm.projectivePresentationOfMapProjectivePresentation _
  (Nonempty.some (H.presentation (F.inverse.obj X)))

Result:
no goals