case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g → f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0

case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0 → Exact f g
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
constructor
no goals
case mp
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g → f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
exact fun h ↦ ⟨h.1, kernel_comp_cokernel f g h⟩
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0 → Exact f g
refine fun h ↦ ⟨h.1, ?_⟩
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))

case hl
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
suffices hl :
  IsLimit (KernelFork.ofι (imageSubobject f).arrow (imageSubobject_arrow_comp_eq_zero h.1))
case hl.refine_1
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
u : W'✝ ⟶ Y
hu : u ≫ g = 0
⊢ W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)

case hl.refine_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ ∀ {W' : C} (g' : W' ⟶ Y) (eq' : g' ≫ g = 0),
    (fun {W'} u hu => ?m.8507 u hu) g' eq' ≫ Subobject.arrow (imageSubobject f) = g'

case hl.refine_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝ = (fun {W'} u hu => ?m.8507 u hu) x✝² x✝¹
case hl
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
refine KernelFork.IsLimit.ofι _ _ (fun u hu ↦ ?_) ?_ (fun _ _ _ h ↦ ?_)
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
this :
  imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
have : imageToKernel f g h.1 = (hl.conePointUniqueUpToIso (limit.isLimit _)).hom ≫
    (kernelSubobjectIso _).inv := by ext; simp
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
this :
  imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
⊢ Epi ((IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv)
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
this :
  imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
⊢ Epi (imageToKernel f g (_ : f ≫ g = 0))
rw [this]
no goals
case mpr
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
this :
  imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
⊢ Epi ((IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv)
infer_instance
case h
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    ((IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv) ≫
      Subobject.arrow (kernelSubobject g)
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) =
    (IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv
ext
no goals
case h
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
hl : IsLimit (KernelFork.ofι (Subobject.arrow (imageSubobject f)) (_ : Subobject.arrow (imageSubobject f) ≫ g = 0))
⊢ imageToKernel f g (_ : f ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    ((IsLimit.conePointUniqueUpToIso hl (limit.isLimit (parallelPair g 0))).hom ≫ (kernelSubobjectIso g).inv) ≫
      Subobject.arrow (kernelSubobject g)
simp
case hl.refine_1
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
u : W'✝ ⟶ Y
hu : u ≫ g = 0
⊢ u ≫ cokernel.π f = 0
case hl.refine_1
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
u : W'✝ ⟶ Y
hu : u ≫ g = 0
⊢ W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
refine kernel.lift (cokernel.π f) u ?_ ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso _).inv
no goals
case hl.refine_1
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
u : W'✝ ⟶ Y
hu : u ≫ g = 0
⊢ u ≫ cokernel.π f = 0
rw [← kernel.lift_ι g u hu, Category.assoc, h.2, comp_zero]
no goals
case hl.refine_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ ∀ {W' : C} (g' : W' ⟶ Y) (eq' : g' ≫ g = 0),
    (fun {W'} u hu =>
            kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
          g' eq' ≫
        Subobject.arrow (imageSubobject f) =
      g'
aesop_cat
case hl.refine_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝ =
    (fun {W'} u hu =>
        kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
      x✝² x✝¹
case hl.refine_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝ =
    (fun {W'} u hu =>
        kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
      x✝² x✝¹
intros
case hl.refine_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝² =
    (fun {W'} u hu =>
          kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
        x✝² x✝¹ ≫
      Subobject.arrow (imageSubobject f)
case hl.refine_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝ =
    (fun {W'} u hu =>
        kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
      x✝² x✝¹
rw [← cancel_mono (imageSubobject f).arrow, h]
no goals
case hl.refine_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h✝ : f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
W'✝ : C
x✝² : W'✝ ⟶ Y
x✝¹ : x✝² ≫ g = 0
x✝ : W'✝ ⟶ Subobject.underlying.obj (imageSubobject f)
h : x✝ ≫ Subobject.arrow (imageSubobject f) = x✝²
⊢ x✝² =
    (fun {W'} u hu =>
          kernel.lift (cokernel.π f) u (_ : u ≫ cokernel.π f = 0) ≫ (imageIsoImage f).hom ≫ (imageSubobjectIso f).inv)
        x✝² x✝¹ ≫
      Subobject.arrow (imageSubobject f)
simp