-- Mathlib/CategoryTheory/Preadditive/Projective/LiftingProperties.lean
lemma projective_iff_llp_epimorphisms_of_isZero
    [HasZeroMorphisms C] {P Z : C} (i : Z ⟶ P) (hZ : IsZero Z) :
    Projective P ↔ (MorphismProperty.epimorphisms C).llp i

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ Projective P → (MorphismProperty.epimorphisms C).llp 0

Tactic:
intro _ X Y p (_ : Epi p)

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
a✝ : Projective P
X Y : C
p : X ⟶ Y
x✝ : Epi p
⊢ HasLiftingProperty 0 p

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
⊢ ∃ f', f' ≫ p = f

Tactic:
have := h _ hp

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
⊢ ∃ f', f' ≫ p = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ Projective P ↔ (MorphismProperty.epimorphisms C).llp 0

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ Projective P → (MorphismProperty.epimorphisms C).llp 0

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ (MorphismProperty.epimorphisms C).llp 0 → Projective P

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ (MorphismProperty.epimorphisms C).llp 0 → Projective P

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
⊢ Projective P

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
⊢ ∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f

Tactic:
intro X Y f p hp

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
⊢ ∃ f', f' ≫ p = f

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
⊢ ∃ f', f' ≫ p = f

Tactic:
have sq : CommSq 0 (0 : Z ⟶ P) p f := ⟨by simp⟩

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
sq : CommSq 0 0 p f
⊢ ∃ f', f' ≫ p = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
i : Z ⟶ P
hZ : IsZero Z
⊢ Projective P ↔ (MorphismProperty.epimorphisms C).llp i

Tactic:
obtain rfl := hZ.eq_of_src i 0

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
⊢ Projective P ↔ (MorphismProperty.epimorphisms C).llp 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
⊢ 0 ≫ p = 0 ≫ f

Tactic:
simp

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
⊢ Projective P

Tactic:
constructor

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
⊢ ∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [inst : Epi e], ∃ f', f' ≫ e = f

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
a✝ : Projective P
X Y : C
p : X ⟶ Y
x✝ : Epi p
⊢ HasLiftingProperty 0 p

Tactic:
exact Projective.hasLiftingProperty_of_isZero 0 p hZ

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
sq : CommSq 0 0 p f
⊢ sq.lift ≫ p = f

Tactic:
simp

Result:
no goals

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X Y : C
f : P ⟶ Y
p : X ⟶ Y
hp : Epi p
this : HasLiftingProperty 0 p
sq : CommSq 0 0 p f
⊢ ∃ f', f' ≫ p = f

Tactic:
exact ⟨sq.lift, by simp⟩

Result:
no goals