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
hgh : Exact g h
inst✝ : Epi f
⊢ 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
hgh : Exact g h
inst✝ : Epi f
⊢ Exact (f ≫ g) h
refine' ⟨by simp [hgh.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
hgh : Exact g h
inst✝ : Epi f
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)

case 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
hgh : Exact g h
inst✝ : Epi 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
hgh : Exact g h
inst✝ : Epi f
⊢ Epi (imageToKernel (f ≫ g) h (_ : (f ≫ g) ≫ h = 0))
rw [imageToKernel_comp_left]
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
hgh : Exact g h
inst✝ : Epi f
this : Epi (imageToKernel g h (_ : g ≫ h = 0))
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)

case 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
hgh : Exact g h
inst✝ : Epi 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
hgh : Exact g h
inst✝ : Epi f
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)

case 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
hgh : Exact g h
inst✝ : Epi f
⊢ g ≫ h = 0
haveI := hgh.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
hgh : Exact g h
inst✝ : Epi f
this : Epi (imageToKernel g h (_ : g ≫ h = 0))
⊢ Epi
    (Subobject.ofLE (imageSubobject (f ≫ g)) (imageSubobject g) (_ : imageSubobject (f ≫ g) ≤ imageSubobject g) ≫
      imageToKernel g h ?w)

case 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
hgh : Exact g h
inst✝ : Epi f
⊢ g ≫ h = 0
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
hgh : Exact g h
inst✝ : Epi f
⊢ (f ≫ g) ≫ h = 0
simp [hgh.w]