[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) = F.map 0
[PROOFSTEP]
have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by rw [← Category.assoc, eq_whisker hf.w]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : NormalMono.Z (F.map f) ⟶ W
⊢ F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
[PROOFSTEP]
rw [← Category.assoc, eq_whisker hf.w]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
reassoc' : ∀ {W : D} (h : NormalMono.Z (F.map f) ⟶ W), F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
⊢ F.map (f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) = F.map 0
[PROOFSTEP]
simp [reassoc']
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) ≫
      (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).hom =
    NormalMono.g
[PROOFSTEP]
simp only [Full.witness, Category.assoc, Iso.inv_hom_id, Category.comp_id]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ KernelFork.ofι
      (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
        𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero))
      (_ :
        (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
              𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero)) ≫
            F.map (Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) =
          0) ≅
    (Cones.postcomposeEquivalence (compNatIso F)).functor.obj
      (F.mapCone
        (KernelFork.ofι f
          (_ : f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv) = 0)))
[PROOFSTEP]
apply Iso.symm
[GOAL]
case I
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ (Cones.postcomposeEquivalence (compNatIso F)).functor.obj
      (F.mapCone
        (KernelFork.ofι f
          (_ : f ≫ Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv) = 0))) ≅
    KernelFork.ofι
      (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
        𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero))
      (_ :
        (Fork.ι (KernelFork.ofι (F.map f) (_ : F.map f ≫ NormalMono.g = 0)) ≫
              𝟙 ((parallelPair NormalMono.g 0).obj WalkingParallelPair.zero)) ≫
            F.map (Full.preimage (NormalMono.g ≫ (Functor.objObjPreimageIso F (NormalMono.Z (F.map f))).inv)) =
          0)
[PROOFSTEP]
apply isoOfι
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
f : X ⟶ Y
I : NormalMono f
⊢ f ≫ g = f ≫ 0
[PROOFSTEP]
simpa using I.w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ NormalMono.g = 0
[PROOFSTEP]
have reassoc' {W : C} (h' : S ⟶ W) : f ≫ h ≫ h' = g ≫ k ≫ h' := by simp only [← Category.assoc, eq_whisker comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
W : C
h' : S ⟶ W
⊢ f ≫ h ≫ h' = g ≫ k ≫ h'
[PROOFSTEP]
simp only [← Category.assoc, eq_whisker comm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
reassoc' : ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'
⊢ g ≫ k ≫ NormalMono.g = 0
[PROOFSTEP]
rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (KernelFork.ofι g (_ : g ≫ k ≫ NormalMono.g = 0))
[PROOFSTEP]
letI gr := regularOfIsPullbackSndOfRegular comm t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular comm t
⊢ IsLimit (KernelFork.ofι g (_ : g ≫ k ≫ NormalMono.g = 0))
[PROOFSTEP]
have q := (HasZeroMorphisms.comp_zero k hn.Z).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular comm t
q : 0 = k ≫ 0
⊢ IsLimit (KernelFork.ofι g (_ : g ≫ k ≫ NormalMono.g = 0))
[PROOFSTEP]
convert gr.isLimit
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ RegularMono f
[PROOFSTEP]
haveI := normalMonoOfMono f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
this : NormalMono f
⊢ RegularMono f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f) = F.map 0
[PROOFSTEP]
simp [hf.w]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ (Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).symm.hom ≫
      F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g)) =
    NormalEpi.g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ CokernelCofork.ofπ
      (𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
        Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)))
      (_ :
        F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g)) ≫
            𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
              Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)) =
          0) ≅
    (Cocones.precomposeEquivalence (compNatIso F).symm).functor.obj
      (F.mapCocone
        (CokernelCofork.ofπ f
          (_ : Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f = 0)))
[PROOFSTEP]
apply Iso.symm
[GOAL]
case I
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsEquivalence F
X Y : C
f : X ⟶ Y
hf : NormalEpi (F.map f)
⊢ (Cocones.precomposeEquivalence (compNatIso F).symm).functor.obj
      (F.mapCocone
        (CokernelCofork.ofπ f
          (_ : Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g) ≫ f = 0))) ≅
    CokernelCofork.ofπ
      (𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
        Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)))
      (_ :
        F.map (Full.preimage ((Functor.objObjPreimageIso F (NormalEpi.W (F.map f))).hom ≫ NormalEpi.g)) ≫
            𝟙 ((parallelPair NormalEpi.g 0).obj WalkingParallelPair.one) ≫
              Cofork.π (CokernelCofork.ofπ (F.map f) (_ : NormalEpi.g ≫ F.map f = 0)) =
          0)
[PROOFSTEP]
apply isoOfπ
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
f : X ⟶ Y
I : NormalEpi f
⊢ g ≫ f = 0 ≫ f
[PROOFSTEP]
simpa using I.w
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (NormalEpi.g ≫ f) ≫ h = 0
[PROOFSTEP]
have reassoc' {W : C} (h' : R ⟶ W) : gn.g ≫ g ≫ h' = 0 ≫ h' := by rw [← Category.assoc, eq_whisker gn.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
⊢ NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
[PROOFSTEP]
rw [← Category.assoc, eq_whisker gn.w]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
⊢ (NormalEpi.g ≫ f) ≫ h = 0
[PROOFSTEP]
rw [Category.assoc, comm, reassoc', zero_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (CokernelCofork.ofπ h (_ : (NormalEpi.g ≫ f) ≫ h = 0))
[PROOFSTEP]
letI hn := regularOfIsPushoutSndOfRegular comm t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular comm t
⊢ IsColimit (CokernelCofork.ofπ h (_ : (NormalEpi.g ≫ f) ≫ h = 0))
[PROOFSTEP]
have q := (@zero_comp _ _ _ gn.W _ _ f).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
hn : RegularEpi h := regularOfIsPushoutSndOfRegular comm t
q : 0 = 0 ≫ f
⊢ IsColimit (CokernelCofork.ofπ h (_ : (NormalEpi.g ≫ f) ≫ h = 0))
[PROOFSTEP]
convert hn.isColimit
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
⊢ ∀ {Z' : Cᵒᵖ} (g' : X ⟶ Z') (eq' : NormalMono.g.op ≫ g' = 0) (m_1 : Y ⟶ Z'),
    f ≫ m_1 = g' →
      m_1 =
        (fun {Z'} g' w' =>
            (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop
                  (_ : { unop := g'.unop ≫ NormalMono.g }.unop = { unop := 0 }.unop))).op)
          g' eq'
[PROOFSTEP]
rintro Z' g' w' m' rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m' =
    (fun {Z'} g' w' =>
        (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop
              (_ : { unop := g'.unop ≫ NormalMono.g }.unop = { unop := 0 }.unop))).op)
      (f ≫ m') w'
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop =
    ((fun {Z'} g' w' =>
          (↑(KernelFork.IsLimit.lift' NormalMono.isLimit g'.unop
                (_ : { unop := g'.unop ≫ NormalMono.g }.unop = { unop := 0 }.unop))).op)
        (f ≫ m') w').unop
[PROOFSTEP]
apply m.isLimit.uniq (KernelFork.ofι (m'.unop ≫ f.unop) _) m'.unop
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ ∀ (j : WalkingParallelPair),
    m'.unop ≫ NatTrans.app (KernelFork.ofι f.unop (_ : f.unop ≫ NormalMono.g = 0)).π j =
      NatTrans.app
        (KernelFork.ofι (m'.unop ≫ f.unop) (_ : { unop := (f ≫ m').unop ≫ NormalMono.g }.unop = { unop := 0 }.unop)).π j
[PROOFSTEP]
rintro (⟨⟩ | ⟨⟩)
[GOAL]
case a.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop ≫ NatTrans.app (KernelFork.ofι f.unop (_ : f.unop ≫ NormalMono.g = 0)).π WalkingParallelPair.zero =
    NatTrans.app
      (KernelFork.ofι (m'.unop ≫ f.unop) (_ : { unop := (f ≫ m').unop ≫ NormalMono.g }.unop = { unop := 0 }.unop)).π
      WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case a.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalMono f.unop
Z' : Cᵒᵖ
m' : Y ⟶ Z'
w' : NormalMono.g.op ≫ f ≫ m' = 0
⊢ m'.unop ≫ NatTrans.app (KernelFork.ofι f.unop (_ : f.unop ≫ NormalMono.g = 0)).π WalkingParallelPair.one =
    NatTrans.app
      (KernelFork.ofι (m'.unop ≫ f.unop) (_ : { unop := (f ≫ m').unop ≫ NormalMono.g }.unop = { unop := 0 }.unop)).π
      WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
⊢ ∀ {W' : Cᵒᵖ} (g' : W' ⟶ Y) (eq' : g' ≫ NormalEpi.g.op = 0) (m_1 : W' ⟶ X),
    m_1 ≫ f = g' →
      m_1 =
        (fun {W'} g' w' =>
            (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop
                  (_ : { unop := NormalEpi.g ≫ g'.unop }.unop = { unop := 0 }.unop))).op)
          g' eq'
[PROOFSTEP]
rintro Z' g' w' m' rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ m' =
    (fun {W'} g' w' =>
        (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop
              (_ : { unop := NormalEpi.g ≫ g'.unop }.unop = { unop := 0 }.unop))).op)
      (m' ≫ f) w'
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ m'.unop =
    ((fun {W'} g' w' =>
          (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop
                (_ : { unop := NormalEpi.g ≫ g'.unop }.unop = { unop := 0 }.unop))).op)
        (m' ≫ f) w').unop
[PROOFSTEP]
apply m.isColimit.uniq (CokernelCofork.ofπ (f.unop ≫ m'.unop) _) m'.unop
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ ∀ (j : WalkingParallelPair),
    NatTrans.app (CokernelCofork.ofπ f.unop (_ : NormalEpi.g ≫ f.unop = 0)).ι j ≫ m'.unop =
      NatTrans.app
        (CokernelCofork.ofπ (f.unop ≫ m'.unop)
            (_ : { unop := NormalEpi.g ≫ (m' ≫ f).unop }.unop = { unop := 0 }.unop)).ι
        j
[PROOFSTEP]
rintro (⟨⟩ | ⟨⟩)
[GOAL]
case a.zero
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ NatTrans.app (CokernelCofork.ofπ f.unop (_ : NormalEpi.g ≫ f.unop = 0)).ι WalkingParallelPair.zero ≫ m'.unop =
    NatTrans.app
      (CokernelCofork.ofπ (f.unop ≫ m'.unop) (_ : { unop := NormalEpi.g ≫ (m' ≫ f).unop }.unop = { unop := 0 }.unop)).ι
      WalkingParallelPair.zero
[PROOFSTEP]
simp
[GOAL]
case a.one
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
Z' : Cᵒᵖ
m' : Z' ⟶ X
w' : (m' ≫ f) ≫ NormalEpi.g.op = 0
⊢ NatTrans.app (CokernelCofork.ofπ f.unop (_ : NormalEpi.g ≫ f.unop = 0)).ι WalkingParallelPair.one ≫ m'.unop =
    NatTrans.app
      (CokernelCofork.ofπ (f.unop ≫ m'.unop) (_ : { unop := NormalEpi.g ≫ (m' ≫ f).unop }.unop = { unop := 0 }.unop)).ι
      WalkingParallelPair.one
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ RegularEpi f
[PROOFSTEP]
haveI := normalEpiOfEpi f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : NormalEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
this : NormalEpi f
⊢ RegularEpi f
[PROOFSTEP]
infer_instance
