case mp
C : Type u₁
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughInjectives C → EnoughInjectives D

case mpr
C : Type u₁
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughInjectives D → EnoughInjectives C
C : Type u₁
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughInjectives C ↔ EnoughInjectives D
constructor
case mp.presentation.val
C : Type u₁
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughInjectives C
X : D
⊢ InjectivePresentation X

case mpr.presentation.val
C : Type u₁
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
F✝ F : C ≌ D
H : EnoughInjectives D
X : C
⊢ InjectivePresentation X
case mp
C : Type u₁
inst✝¹ : Category C
D : Type u_2
inst✝ : Category D
F✝ F : C ≌ D
⊢ EnoughInjectives C → EnoughInjectives D

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