V : Type u
inst✝³ : Category V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        imageToKernel f g (_ : f ≫ g = 0) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ IsIso (imageToKernel f g (_ : f ≫ g = 0))
refine' ⟨⟨Subobject.ofLE _ _ p.ge, _⟩⟩
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        imageToKernel f g (_ : f ≫ g = 0) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
dsimp [imageToKernel]
no goals
V : Type u
inst✝³ : Category V
inst✝² : HasImages V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasKernels V
A B C : V
f : A ⟶ B
g : B ⟶ C
p : imageSubobject f = kernelSubobject g
⊢ Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) ≫
        Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) =
      𝟙 (Subobject.underlying.obj (imageSubobject f)) ∧
    Subobject.ofLE (kernelSubobject g) (imageSubobject f) (_ : kernelSubobject g ≤ imageSubobject f) ≫
        Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g) =
      𝟙 (Subobject.underlying.obj (kernelSubobject g))
simp only [Subobject.ofLE_comp_ofLE, Subobject.ofLE_refl]