-- Mathlib/CategoryTheory/Preadditive/Injective/LiftingProperties.lean
lemma injective_iff_rlp_monomorphisms_of_isZero
    [HasZeroMorphisms C] {I Z : C} (p : I ⟶ Z) (hZ : IsZero Z) :
    Injective I ↔ (MorphismProperty.monomorphisms C).rlp p

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ (MorphismProperty.monomorphisms C).rlp 0 → Injective I

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
⊢ Injective I

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
a✝ : Injective I
A B : C
i : A ⟶ B
x✝ : Mono i
⊢ HasLiftingProperty i 0

Tactic:
exact Injective.hasLiftingProperty_of_isZero i 0 hZ

Result:
no goals

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
⊢ ∀ {X Y : C} (g : X ⟶ I) (f : X ⟶ Y) [inst : Mono f], ∃ h, f ≫ h = g

Tactic:
intro A B f i hi

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
⊢ ∃ h, i ≫ h = f

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ Injective I → (MorphismProperty.monomorphisms C).rlp 0

Tactic:
intro _ A B i (_ : Mono i)

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
a✝ : Injective I
A B : C
i : A ⟶ B
x✝ : Mono i
⊢ HasLiftingProperty i 0

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty i 0
sq : CommSq f i 0 0
⊢ ∃ h, i ≫ h = f

Tactic:
exact ⟨sq.lift, by simp⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty i 0
sq : CommSq f i 0 0
⊢ i ≫ sq.lift = f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
p : I ⟶ Z
hZ : IsZero Z
⊢ Injective I ↔ (MorphismProperty.monomorphisms C).rlp p

Tactic:
obtain rfl := hZ.eq_of_tgt p 0

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ Injective I ↔ (MorphismProperty.monomorphisms C).rlp 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty i 0
⊢ f ≫ 0 = i ≫ 0

Tactic:
simp

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
⊢ Injective I

Tactic:
constructor

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
⊢ ∀ {X Y : C} (g : X ⟶ I) (f : X ⟶ Y) [inst : Mono f], ∃ h, f ≫ h = g

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
⊢ ∃ h, i ≫ h = f

Tactic:
have := h _ hi

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty i 0
⊢ ∃ h, i ≫ h = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ Injective I ↔ (MorphismProperty.monomorphisms C).rlp 0

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ Injective I → (MorphismProperty.monomorphisms C).rlp 0

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ (MorphismProperty.monomorphisms C).rlp 0 → Injective I

Proof state:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty i 0
⊢ ∃ h, i ≫ h = f

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

Result:
case mpr.factors
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
A B : C
f : A ⟶ I
i : A ⟶ B
hi : Mono i
this : HasLiftingProperty i 0
sq : CommSq f i 0 0
⊢ ∃ h, i ≫ h = f