case mp
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ factorThru P f h = 0 → f = 0

case mpr
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ f = 0 → factorThru P f h = 0
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ factorThru P f h = 0 ↔ f = 0
fconstructor
case mp
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h = 0
⊢ f = 0
case mp
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ factorThru P f h = 0 → f = 0
intro w
case mp
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h ≫ arrow P = 0 ≫ arrow P
⊢ f = 0
case mp
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h = 0
⊢ f = 0
replace w := w =≫ P.arrow
no goals
case mp
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h ≫ arrow P = 0 ≫ arrow P
⊢ f = 0
simpa using w
case mpr
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h = 0
case mpr
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ f = 0 → factorThru P f h = 0
rintro rfl
case mpr.h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h ≫ arrow P = 0 ≫ arrow P
case mpr
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h = 0
ext
no goals
case mpr.h
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h ≫ arrow P = 0 ≫ arrow P
simp