V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
g : 0 ⟶ C
⊢ Exact 0 g
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B C✝ D : V
f✝ : A✝ ⟶ B
g✝ : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
f : A ⟶ 0
g : 0 ⟶ C
⊢ Exact f g
obtain rfl : f = 0 := by ext
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Exact 0 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✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
g : 0 ⟶ C
⊢ Exact 0 g
obtain rfl : g = 0 := by ext
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✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ 0 ≫ 0 = 0

case epi
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Epi (imageToKernel 0 0 ?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✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Exact 0 0
fconstructor
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✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
f : A ⟶ 0
g : 0 ⟶ C
⊢ f = 0
ext
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✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
g : 0 ⟶ C
⊢ g = 0
ext
no goals
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✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ 0 ≫ 0 = 0
simp
no goals
case epi
V : Type u
inst✝⁴ : Category V
inst✝³ : HasImages V
A✝ B C✝ D : V
f : A✝ ⟶ B
g : B ⟶ C✝
h : C✝ ⟶ D
inst✝² : HasZeroObject V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A C : V
⊢ Epi (imageToKernel 0 0 (_ : 0 ≫ 0 = 0))
exact imageToKernel_epi_of_zero_of_mono 0