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
hfg : Exact f g
inst✝ : Mono h
⊢ Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 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
hfg : Exact f g
inst✝ : Mono h
⊢ Exact f (g ≫ h)
refine' ⟨by simp [hfg.w_assoc], _⟩
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
hfg : Exact f g
inst✝ : Mono h
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ 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
hfg : Exact f g
inst✝ : Mono h
⊢ Epi (imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0))
rw [imageToKernel_comp_right f g h hfg.w]
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
hfg : Exact f g
inst✝ : Mono h
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ 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
hfg : Exact f g
inst✝ : Mono h
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h)))
haveI := hfg.epi
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
hfg : Exact f g
inst✝ : Mono h
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ Epi
    (imageToKernel f g (_ : f ≫ g = 0) ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h)))
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
hfg : Exact f g
inst✝ : Mono h
⊢ f ≫ g ≫ h = 0
simp [hfg.w_assoc]