V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
⊢ Exact f (g ≫ h) ↔ Exact f g
refine'
  ⟨fun hfg => ⟨zero_of_comp_mono h (by rw [Category.assoc, hfg.1]), _⟩, fun h =>
    exact_comp_mono h⟩
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
rw [← (Iso.eq_comp_inv _).1 (imageToKernel_comp_mono _ _ h hfg.1)]
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
this : Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0))
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
haveI := hfg.2
no goals
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
this : Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0))
⊢ Epi
    (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).hom)
infer_instance
no goals
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A B C D : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
inst✝² : HasZeroMorphisms V
inst✝¹ : HasEqualizers V
inst✝ : Mono h
hfg : Exact f (g ≫ h)
⊢ (f ≫ g) ≫ h = 0
rw [Category.assoc, hfg.1]