[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ (imageMonoFactorisation f).e = cokernel.π (kernel.ι f) ≫ coimageImageComparison f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) = cokernel.π (kernel.ι f) ≫ coimageImageComparison f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) ≫ equalizer.ι (cokernel.π f) 0 =
    (cokernel.π (kernel.ι f) ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0
[PROOFSTEP]
simp only [Abelian.coimageImageComparison, imageMonoFactorisation_e, Category.assoc, cokernel.π_desc_assoc]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ (fun F => inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e (_ : kernel.ι f ≫ F.e = 0)) F ≫ F.m =
    (imageMonoFactorisation f).m
[PROOFSTEP]
rw [imageMonoFactorisation_m]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ (fun F => inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e (_ : kernel.ι f ≫ F.e = 0)) F ≫ F.m =
    kernel.ι (cokernel.π f)
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e (_ : kernel.ι f ≫ F.e = 0) ≫ F.m =
    kernel.ι (cokernel.π f)
[PROOFSTEP]
rw [IsIso.inv_comp_eq]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ cokernel.desc (kernel.ι f) F.e (_ : kernel.ι f ≫ F.e = 0) ≫ F.m = coimageImageComparison f ≫ kernel.ι (cokernel.π f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) F.e (_ : kernel.ι f ≫ F.e = 0) ≫ F.m =
    coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f ≫ kernel.ι (cokernel.π f)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasKernels C
inst✝³ : HasCokernels C
inst✝² : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsIso (coimageImageComparison f)
⊢ IsIso (imageMonoFactorisation f).e
[PROOFSTEP]
rw [imageMonoFactorisation_e']
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasKernels C
inst✝³ : HasCokernels C
inst✝² : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsIso (coimageImageComparison f)
⊢ IsIso (cokernel.π (kernel.ι f) ≫ coimageImageComparison f)
[PROOFSTEP]
exact IsIso.comp_isIso
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ IsIso (imageMonoFactorisation f).m
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : HasZeroObject C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ IsIso (kernel.ι (cokernel.π f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
⊢ f ≫ cokernel.π f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
⊢ IsLimit (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0))
[PROOFSTEP]
haveI : Limits.HasImages C := hasImages
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this : HasImages C
⊢ IsLimit (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0))
[PROOFSTEP]
haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝ : HasImages C
this : HasEqualizers C
⊢ IsLimit (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0))
[PROOFSTEP]
haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ IsLimit (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0))
[PROOFSTEP]
have aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f (by simp)) =
      Fork.ι s :=
  ?_
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : KernelFork (cokernel.π f)
⊢ f ≫ cokernel.π f = 0
[PROOFSTEP]
simp
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) =
      Fork.ι s
⊢ IsLimit (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0))
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) =
      Fork.ι s
[PROOFSTEP]
refine' isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux _
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) =
      Fork.ι s
⊢ ∀ (s : KernelFork (cokernel.π f)) (m_1 : s.pt ⟶ (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)).pt),
    m_1 ≫ Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) = Fork.ι s →
      m_1 = (fun A => limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) s
[PROOFSTEP]
intro A g hg
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)).pt
hg : g ≫ Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) = Fork.ι A
⊢ g = (fun A => limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) A
[PROOFSTEP]
rw [KernelFork.ι_ofι] at hg
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) =
      Fork.ι s
A : KernelFork (cokernel.π f)
g : A.pt ⟶ (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)).pt
hg : g ≫ f = Fork.ι A
⊢ g = (fun A => limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) A
[PROOFSTEP]
rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
[GOAL]
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ ∀ (s : KernelFork (cokernel.π f)),
    (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
        Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) =
      Fork.ι s
[PROOFSTEP]
intro A
[GOAL]
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : KernelFork (cokernel.π f)
⊢ (limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e) ≫
      Fork.ι (KernelFork.ofι f (_ : f ≫ cokernel.π f = 0)) =
    Fork.ι A
[PROOFSTEP]
simp only [KernelFork.ι_ofι, Category.assoc]
[GOAL]
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : KernelFork (cokernel.π f)
⊢ limit.lift (parallelPair (cokernel.π f) 0) A ≫ inv (imageMonoFactorisation f).e ≫ f = Fork.ι A
[PROOFSTEP]
convert limit.lift_π A WalkingParallelPair.zero using 2
[GOAL]
case h.e'_2.h.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : KernelFork (cokernel.π f)
⊢ inv (imageMonoFactorisation f).e ≫ f = limit.π (parallelPair (cokernel.π f) 0) WalkingParallelPair.zero
[PROOFSTEP]
rw [IsIso.inv_comp_eq, eq_comm]
[GOAL]
case h.e'_2.h.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : KernelFork (cokernel.π f)
⊢ (imageMonoFactorisation f).e ≫ limit.π (parallelPair (cokernel.π f) 0) WalkingParallelPair.zero = f
[PROOFSTEP]
exact (imageMonoFactorisation f).fac
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
⊢ IsColimit (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0))
[PROOFSTEP]
haveI : Limits.HasImages C := hasImages
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this : HasImages C
⊢ IsColimit (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0))
[PROOFSTEP]
haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝ : HasImages C
this : HasEqualizers C
⊢ IsColimit (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0))
[PROOFSTEP]
haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ IsColimit (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0))
[PROOFSTEP]
have aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f (by simp)) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (Abelian.coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s :=
  ?_
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
⊢ kernel.ι f ≫ f = 0
[PROOFSTEP]
simp
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
⊢ IsColimit (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0))
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
[PROOFSTEP]
refine'
  isColimitAux _ (fun A => inv (imageMonoFactorisation f).m ≫ inv (Abelian.coimageImageComparison f) ≫ colimit.desc _ _)
    aux _
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
⊢ ∀ (s : CokernelCofork (kernel.ι f)) (m_1 : (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)).pt ⟶ s.pt),
    Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫ m_1 = Cofork.π s →
      m_1 =
        (fun A =>
            inv (imageMonoFactorisation f).m ≫
              inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A)
          s
[PROOFSTEP]
intro A g hg
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)).pt ⟶ A.pt
hg : Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫ g = Cofork.π A
⊢ g =
    (fun A =>
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A)
      A
[PROOFSTEP]
rw [CokernelCofork.π_ofπ] at hg
[GOAL]
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ g =
    (fun A =>
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A)
      A
[PROOFSTEP]
rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]
[GOAL]
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
⊢ ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
[PROOFSTEP]
intro A
[GOAL]
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : CokernelCofork (kernel.ι f)
⊢ Cofork.π (CokernelCofork.ofπ f (_ : kernel.ι f ≫ f = 0)) ≫
      inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A =
    Cofork.π A
[PROOFSTEP]
simp only [CokernelCofork.π_ofπ, ← Category.assoc]
[GOAL]
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : CokernelCofork (kernel.ι f)
⊢ ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f)) ≫
      colimit.desc (parallelPair (kernel.ι f) 0) A =
    Cofork.π A
[PROOFSTEP]
convert colimit.ι_desc A WalkingParallelPair.one using 2
[GOAL]
case h.e'_2.h.e'_6
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : CokernelCofork (kernel.ι f)
⊢ (f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f) =
    colimit.ι (parallelPair (kernel.ι f) 0) WalkingParallelPair.one
[PROOFSTEP]
rw [IsIso.comp_inv_eq, IsIso.comp_inv_eq, eq_comm, ← imageMonoFactorisation_e']
[GOAL]
case h.e'_2.h.e'_6
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
A : CokernelCofork (kernel.ι f)
⊢ (imageMonoFactorisation f).e ≫ (imageMonoFactorisation f).m = f
[PROOFSTEP]
exact (imageMonoFactorisation f).fac
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Epi (Abelian.factorThruImage f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
⊢ IsIso (Abelian.factorThruImage f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Mono (Abelian.factorThruCoimage f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
⊢ IsIso (Abelian.factorThruCoimage f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ Epi f
[PROOFSTEP]
apply NormalMonoCategory.epi_of_zero_cokernel _ (cokernel f)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ IsColimit (CokernelCofork.ofπ 0 (_ : f ≫ 0 = 0))
[PROOFSTEP]
simp_rw [← h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ IsColimit (CokernelCofork.ofπ (cokernel.π f) (_ : f ≫ cokernel.π f = 0))
[PROOFSTEP]
exact IsColimit.ofIsoColimit (colimit.isColimit (parallelPair f 0)) (isoOfπ _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ Abelian.factorThruImage f ≫ image.ι f ≫ g = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
R : C
g : Q ⟶ R
h : f ≫ g = 0
⊢ (f ≫ coimage.π g) ≫ Abelian.factorThruCoimage g = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Mono (image.ι f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Mono (Abelian.factorThruCoimage f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ HasImages C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ HasImageMaps C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ IsIso (coimageImageComparison f)
[PROOFSTEP]
convert
  IsIso.of_iso
    (IsImage.isoExt (coimageStrongEpiMonoFactorisation f).toMonoIsImage
      (imageStrongEpiMonoFactorisation f).toMonoIsImage)
[GOAL]
case h.e'_5.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
e_3✝ : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).toMonoFactorisation.I
e_4✝ : Abelian.image f = (imageStrongEpiMonoFactorisation f).toMonoFactorisation.I
⊢ coimageImageComparison f =
    (IsImage.isoExt (StrongEpiMonoFactorisation.toMonoIsImage (coimageStrongEpiMonoFactorisation f))
        (StrongEpiMonoFactorisation.toMonoIsImage (imageStrongEpiMonoFactorisation f))).hom
[PROOFSTEP]
ext
[GOAL]
case h.e'_5.h.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
e_3✝ : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).toMonoFactorisation.I
e_4✝ : Abelian.image f = (imageStrongEpiMonoFactorisation f).toMonoFactorisation.I
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫
        (IsImage.isoExt (StrongEpiMonoFactorisation.toMonoIsImage (coimageStrongEpiMonoFactorisation f))
            (StrongEpiMonoFactorisation.toMonoIsImage (imageStrongEpiMonoFactorisation f))).hom) ≫
      equalizer.ι (cokernel.π f) 0
[PROOFSTEP]
change _ = _ ≫ (imageStrongEpiMonoFactorisation f).m
[GOAL]
case h.e'_5.h.h.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
e_3✝ : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).toMonoFactorisation.I
e_4✝ : Abelian.image f = (imageStrongEpiMonoFactorisation f).toMonoFactorisation.I
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫
        (IsImage.isoExt (StrongEpiMonoFactorisation.toMonoIsImage (coimageStrongEpiMonoFactorisation f))
            (StrongEpiMonoFactorisation.toMonoIsImage (imageStrongEpiMonoFactorisation f))).hom) ≫
      (imageStrongEpiMonoFactorisation f).toMonoFactorisation.m
[PROOFSTEP]
simp [-imageStrongEpiMonoFactorisation_m]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ factorThruImage f = 0
[PROOFSTEP]
simp [← cancel_mono (Limits.image.ι f)]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (coimageIsoImage' f).hom = cokernel.desc (kernel.ι f) (factorThruImage f) (_ : kernel.ι f ≫ factorThruImage f = 0)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι f) 0 ≫ (coimageIsoImage' f).hom =
    coequalizer.π (kernel.ι f) 0 ≫
      cokernel.desc (kernel.ι f) (factorThruImage f) (_ : kernel.ι f ≫ factorThruImage f = 0)
[PROOFSTEP]
simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc, Category.assoc, IsImage.lift_ι,
  coimageStrongEpiMonoFactorisation_m, Limits.image.fac]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ factorThruImage f ≫ (coimageIsoImage' f).inv = cokernel.π (kernel.ι f)
[PROOFSTEP]
simp only [IsImage.isoExt_inv, image.isImage_lift, image.fac_lift, coimageStrongEpiMonoFactorisation_e]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageIsoImage f).hom ≫ Limits.image.ι f = kernel.ι (cokernel.π f)
[PROOFSTEP]
simp only [IsImage.isoExt_hom, IsImage.lift_ι, imageStrongEpiMonoFactorisation_m]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Limits.image.ι f ≫ cokernel.π f = 0
[PROOFSTEP]
simp [← cancel_epi (factorThruImage f)]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageIsoImage f).inv = kernel.lift (cokernel.π f) (Limits.image.ι f) (_ : Limits.image.ι f ≫ cokernel.π f = 0)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (factorThruImage f ≫ (imageIsoImage f).inv) ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) (_ : Limits.image.ι f ≫ cokernel.π f = 0)) ≫
      equalizer.ι (cokernel.π f) 0
[PROOFSTEP]
rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift, imageStrongEpiMonoFactorisation_e, Category.assoc,
  kernel.lift_ι, equalizer_as_kernel, kernel.lift_ι, Limits.image.fac]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ pullbackToBiproduct f g ≫ biprod.desc f (-g) = 0
[PROOFSTEP]
rw [biprod.lift_desc, comp_neg, pullback.condition, add_right_neg]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (Fork.ι s ≫ biprod.fst) ≫ f - (Fork.ι s ≫ biprod.snd) ≫ g = 0
[PROOFSTEP]
rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ← biprod.desc_eq, KernelFork.condition s]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (fun s =>
          pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
            (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
        s ≫
      Fork.ι (pullbackToBiproductFork f g) =
    Fork.ι s
[PROOFSTEP]
apply biprod.hom_ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ ((fun s =>
            pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
              (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
          s ≫
        Fork.ι (pullbackToBiproductFork f g)) ≫
      biprod.fst =
    Fork.ι s ≫ biprod.fst
[PROOFSTEP]
rw [Fork.ι_ofι, Category.assoc]
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ ((fun s =>
            pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
              (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
          s ≫
        Fork.ι (pullbackToBiproductFork f g)) ≫
      biprod.snd =
    Fork.ι s ≫ biprod.snd
[PROOFSTEP]
rw [Fork.ι_ofι, Category.assoc]
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (fun s =>
          pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
            (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
        s ≫
      pullbackToBiproduct f g ≫ biprod.fst =
    Fork.ι s ≫ biprod.fst
[PROOFSTEP]
rw [biprod.lift_fst, pullback.lift_fst]
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ (fun s =>
          pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
            (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
        s ≫
      pullbackToBiproduct f g ≫ biprod.snd =
    Fork.ι s ≫ biprod.snd
[PROOFSTEP]
rw [biprod.lift_snd, pullback.lift_snd]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = Fork.ι s
⊢ m =
    (fun s =>
        pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
          (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
      s
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = Fork.ι s
⊢ m ≫ pullback.fst =
    (fun s =>
          pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
            (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
        s ≫
      pullback.fst
[PROOFSTEP]
simp [← h]
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ (pullbackToBiproductFork f g).pt
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = Fork.ι s
⊢ m ≫ pullback.snd =
    (fun s =>
          pullback.lift (Fork.ι s ≫ biprod.fst) (Fork.ι s ≫ biprod.snd)
            (_ : (Fork.ι s ≫ biprod.fst) ≫ f = (Fork.ι s ≫ biprod.snd) ≫ g))
        s ≫
      pullback.snd
[PROOFSTEP]
simp [← h]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ biprod.lift f (-g) ≫ biproductToPushout f g = 0
[PROOFSTEP]
rw [biprod.lift_desc, neg_comp, pushout.condition, add_right_neg]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ f ≫ biprod.inl ≫ Cofork.π s - g ≫ biprod.inr ≫ Cofork.π s = 0
[PROOFSTEP]
rw [← Category.assoc, ← Category.assoc, ← sub_comp, sub_eq_add_neg, ← neg_comp, ← biprod.lift_eq, Cofork.condition s,
  zero_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ Cofork.π (biproductToPushoutCofork f g) ≫
      (fun s =>
          pushout.desc (biprod.inl ≫ Cofork.π s) (biprod.inr ≫ Cofork.π s)
            (_ : f ≫ biprod.inl ≫ Cofork.π s = g ≫ biprod.inr ≫ Cofork.π s))
        s =
    Cofork.π s
[PROOFSTEP]
apply biprod.hom_ext'
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ biprod.inl ≫
      Cofork.π (biproductToPushoutCofork f g) ≫
        (fun s =>
            pushout.desc (biprod.inl ≫ Cofork.π s) (biprod.inr ≫ Cofork.π s)
              (_ : f ≫ biprod.inl ≫ Cofork.π s = g ≫ biprod.inr ≫ Cofork.π s))
          s =
    biprod.inl ≫ Cofork.π s
[PROOFSTEP]
simp
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
⊢ biprod.inr ≫
      Cofork.π (biproductToPushoutCofork f g) ≫
        (fun s =>
            pushout.desc (biprod.inl ≫ Cofork.π s) (biprod.inr ≫ Cofork.π s)
              (_ : f ≫ biprod.inl ≫ Cofork.π s = g ≫ biprod.inr ≫ Cofork.π s))
          s =
    biprod.inr ≫ Cofork.π s
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = Cofork.π s
⊢ m =
    (fun s =>
        pushout.desc (biprod.inl ≫ Cofork.π s) (biprod.inr ≫ Cofork.π s)
          (_ : f ≫ biprod.inl ≫ Cofork.π s = g ≫ biprod.inr ≫ Cofork.π s))
      s
[PROOFSTEP]
apply pushout.hom_ext
[GOAL]
case h₀
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = Cofork.π s
⊢ pushout.inl ≫ m =
    pushout.inl ≫
      (fun s =>
          pushout.desc (biprod.inl ≫ Cofork.π s) (biprod.inr ≫ Cofork.π s)
            (_ : f ≫ biprod.inl ≫ Cofork.π s = g ≫ biprod.inr ≫ Cofork.π s))
        s
[PROOFSTEP]
simp [← h]
[GOAL]
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = Cofork.π s
⊢ pushout.inr ≫ m =
    pushout.inr ≫
      (fun s =>
          pushout.desc (biprod.inl ≫ Cofork.π s) (biprod.inr ≫ Cofork.π s)
            (_ : f ≫ biprod.inl ≫ Cofork.π s = g ≫ biprod.inr ≫ Cofork.π s))
        s
[PROOFSTEP]
simp [← h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
⊢ e = 0
[PROOFSTEP]
let u := biprod.desc (0 : X ⟶ R) e
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
⊢ e = 0
[PROOFSTEP]
have hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0 := by
  simpa
    -- pullback_to_biproduct f g is a kernel of (f, -g), so (f, -g) is a
        -- cokernel of pullback_to_biproduct f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
⊢ PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
[PROOFSTEP]
simpa
  -- pullback_to_biproduct f g is a kernel of (f, -g), so (f, -g) is a
      -- cokernel of pullback_to_biproduct f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
⊢ e = 0
[PROOFSTEP]
have :=
  epiIsCokernelOfKernel _
    (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)
      -- We use this fact to obtain a factorization of u through (f, -g) via some d : Z ⟶ R.
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
⊢ e = 0
[PROOFSTEP]
obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d :
  (CokernelCofork.ofπ (biprod.desc f (-g))
        (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0)).pt ⟶
    R
hd :
  Cofork.π
        (CokernelCofork.ofπ (biprod.desc f (-g))
          (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0)) ≫
      d =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at d
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd :
  Cofork.π
        (CokernelCofork.ofπ (biprod.desc f (-g))
          (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0)) ≫
      d =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at hd
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
⊢ e = 0
[PROOFSTEP]
have : f ≫ d = 0
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
⊢ f ≫ d = 0
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this : f ≫ d = 0
⊢ e = 0
[PROOFSTEP]
calc
  f ≫ d = (biprod.inl ≫ biprod.desc f (-g)) ≫ d := by rw [biprod.inl_desc]
  _ = biprod.inl ≫ u := by rw [Category.assoc, hd]
  _ = 0 :=
    biprod.inl_desc _
      _
        -- But f is an epimorphism, so d = 0...
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
⊢ f ≫ d = (biprod.inl ≫ biprod.desc f (-g)) ≫ d
[PROOFSTEP]
rw [biprod.inl_desc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
⊢ (biprod.inl ≫ biprod.desc f (-g)) ≫ d = biprod.inl ≫ u
[PROOFSTEP]
rw [Category.assoc, hd]
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this : f ≫ d = 0
⊢ e = 0
[PROOFSTEP]
have : d = 0 :=
  (cancel_epi f).1
    (by simpa)
      -- ...or, in other words, e = 0.
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this : f ≫ d = 0
⊢ f ≫ d = f ≫ 0
[PROOFSTEP]
simpa
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ e = 0
[PROOFSTEP]
calc
  e = biprod.inr ≫ biprod.desc (0 : X ⟶ R) e := by rw [biprod.inr_desc]
  _ = biprod.inr ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
  _ = biprod.inr ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
  _ = (biprod.inr ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
  _ = 0 := HasZeroMorphisms.comp_zero _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ e = biprod.inr ≫ biprod.desc 0 e
[PROOFSTEP]
rw [biprod.inr_desc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ biprod.inr ≫ biprod.desc 0 e = biprod.inr ≫ biprod.desc f (-g) ≫ d
[PROOFSTEP]
rw [← hd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ biprod.inr ≫ biprod.desc f (-g) ≫ d = biprod.inr ≫ biprod.desc f (-g) ≫ 0
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ biprod.inr ≫ biprod.desc f (-g) ≫ 0 = (biprod.inr ≫ biprod.desc f (-g)) ≫ 0
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
⊢ e = 0
[PROOFSTEP]
let u :=
  biprod.desc e
    (0 : Y ⟶ R)
      -- The composite pullback f g ⟶ X ⊞ Y ⟶ R is zero by assumption.
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
⊢ e = 0
[PROOFSTEP]
have hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0 := by
  simpa
    -- pullback_to_biproduct f g is a kernel of (f, -g), so (f, -g) is a
        -- cokernel of pullback_to_biproduct f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
⊢ PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
[PROOFSTEP]
simpa
  -- pullback_to_biproduct f g is a kernel of (f, -g), so (f, -g) is a
      -- cokernel of pullback_to_biproduct f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
⊢ e = 0
[PROOFSTEP]
have :=
  epiIsCokernelOfKernel _
    (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)
      -- We use this fact to obtain a factorization of u through (f, -g) via some d : Z ⟶ R.
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
⊢ e = 0
[PROOFSTEP]
obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d :
  (CokernelCofork.ofπ (biprod.desc f (-g))
        (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0)).pt ⟶
    R
hd :
  Cofork.π
        (CokernelCofork.ofπ (biprod.desc f (-g))
          (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0)) ≫
      d =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at d
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd :
  Cofork.π
        (CokernelCofork.ofπ (biprod.desc f (-g))
          (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0)) ≫
      d =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at hd
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ e = 0
[PROOFSTEP]
have : (-g) ≫ d = 0
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ (-g) ≫ d = 0
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this : (-g) ≫ d = 0
⊢ e = 0
[PROOFSTEP]
calc
  (-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d := by rw [biprod.inr_desc]
  _ = biprod.inr ≫ u := by rw [Category.assoc, hd]
  _ = 0 :=
    biprod.inr_desc _
      _
        -- But g is an epimorphism, thus so is -g, so d = 0...
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ (-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d
[PROOFSTEP]
rw [biprod.inr_desc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ (biprod.inr ≫ biprod.desc f (-g)) ≫ d = biprod.inr ≫ u
[PROOFSTEP]
rw [Category.assoc, hd]
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this : (-g) ≫ d = 0
⊢ e = 0
[PROOFSTEP]
have : d = 0 :=
  (cancel_epi (-g)).1
    (by simpa)
      -- ...or, in other words, e = 0.
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this : (-g) ≫ d = 0
⊢ (-g) ≫ d = (-g) ≫ 0
[PROOFSTEP]
simpa
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ e = 0
[PROOFSTEP]
calc
  e = biprod.inl ≫ biprod.desc e (0 : Y ⟶ R) := by rw [biprod.inl_desc]
  _ = biprod.inl ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
  _ = biprod.inl ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
  _ = (biprod.inl ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
  _ = 0 := HasZeroMorphisms.comp_zero _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ e = biprod.inl ≫ biprod.desc e 0
[PROOFSTEP]
rw [biprod.inl_desc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ biprod.inl ≫ biprod.desc e 0 = biprod.inl ≫ biprod.desc f (-g) ≫ d
[PROOFSTEP]
rw [← hd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ biprod.inl ≫ biprod.desc f (-g) ≫ d = biprod.inl ≫ biprod.desc f (-g) ≫ 0
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ :
  IsColimit
    (CokernelCofork.ofπ (biprod.desc f (-g))
      (_ : Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g) ≫ biprod.desc f (-g) = 0))
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
this✝ : (-g) ≫ d = 0
this : d = 0
⊢ biprod.inl ≫ biprod.desc f (-g) ≫ 0 = (biprod.inl ≫ biprod.desc f (-g)) ≫ 0
[PROOFSTEP]
rw [← Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
⊢ Epi (PullbackCone.snd s)
[PROOFSTEP]
haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.right) := Abelian.epi_pullback_of_epi_f f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
this : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.right)
⊢ Epi (PullbackCone.snd s)
[PROOFSTEP]
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
s : PullbackCone f g
hs : IsLimit s
⊢ Epi (PullbackCone.fst s)
[PROOFSTEP]
haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.left) := Abelian.epi_pullback_of_epi_g f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
s : PullbackCone f g
hs : IsLimit s
this : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.left)
⊢ Epi (PullbackCone.fst s)
[PROOFSTEP]
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g₁ : Y ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : X ⟶ W
hf : f' ≫ g₂ = f
t : PullbackCone f g
ht : IsLimit t
⊢ Epi (PullbackCone.fst t)
[PROOFSTEP]
apply epi_fst_of_isLimit _ _ (PullbackCone.isLimitOfFactors f g g₂ f' g₁ hf hg t ht)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
⊢ e = 0
[PROOFSTEP]
let u := biprod.lift (0 : R ⟶ Y) e
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
⊢ e = 0
[PROOFSTEP]
have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0 := by simpa
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
⊢ u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
⊢ e = 0
[PROOFSTEP]
have := monoIsKernelOfCokernel _ (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
⊢ e = 0
[PROOFSTEP]
obtain ⟨d, hd⟩ := KernelFork.IsLimit.lift' this u hu
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d :
  R ⟶
    (KernelFork.ofι (biprod.lift f (-g))
        (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0)).pt
hd :
  d ≫
      Fork.ι
        (KernelFork.ofι (biprod.lift f (-g))
          (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0)) =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at d
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd :
  d ≫
      Fork.ι
        (KernelFork.ofι (biprod.lift f (-g))
          (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0)) =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at hd
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
⊢ e = 0
[PROOFSTEP]
have : d ≫ f = 0
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
⊢ d ≫ f = 0
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this : d ≫ f = 0
⊢ e = 0
[PROOFSTEP]
calc
  d ≫ f = d ≫ biprod.lift f (-g) ≫ biprod.fst := by rw [biprod.lift_fst]
  _ = u ≫ biprod.fst := by rw [← Category.assoc, hd]
  _ = 0 := biprod.lift_fst _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
⊢ d ≫ f = d ≫ biprod.lift f (-g) ≫ biprod.fst
[PROOFSTEP]
rw [biprod.lift_fst]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
⊢ d ≫ biprod.lift f (-g) ≫ biprod.fst = u ≫ biprod.fst
[PROOFSTEP]
rw [← Category.assoc, hd]
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this : d ≫ f = 0
⊢ e = 0
[PROOFSTEP]
have : d = 0 := (cancel_mono f).1 (by simpa)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this : d ≫ f = 0
⊢ d ≫ f = 0 ≫ f
[PROOFSTEP]
simpa
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this✝ : d ≫ f = 0
this : d = 0
⊢ e = 0
[PROOFSTEP]
calc
  e = biprod.lift (0 : R ⟶ Y) e ≫ biprod.snd := by rw [biprod.lift_snd]
  _ = (d ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [← hd]
  _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd := by rw [this]
  _ = 0 ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [Category.assoc]
  _ = 0 := zero_comp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this✝ : d ≫ f = 0
this : d = 0
⊢ e = biprod.lift 0 e ≫ biprod.snd
[PROOFSTEP]
rw [biprod.lift_snd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this✝ : d ≫ f = 0
this : d = 0
⊢ biprod.lift 0 e ≫ biprod.snd = (d ≫ biprod.lift f (-g)) ≫ biprod.snd
[PROOFSTEP]
rw [← hd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this✝ : d ≫ f = 0
this : d = 0
⊢ (d ≫ biprod.lift f (-g)) ≫ biprod.snd = (0 ≫ biprod.lift f (-g)) ≫ biprod.snd
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
R : C
e : R ⟶ Z
h : e ≫ pushout.inr = 0
u : R ⟶ Y ⊞ Z := biprod.lift 0 e
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift 0 e
this✝ : d ≫ f = 0
this : d = 0
⊢ (0 ≫ biprod.lift f (-g)) ≫ biprod.snd = 0 ≫ biprod.lift f (-g) ≫ biprod.snd
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
⊢ e = 0
[PROOFSTEP]
let u := biprod.lift e (0 : R ⟶ Z)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
⊢ e = 0
[PROOFSTEP]
have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0 := by simpa
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
⊢ u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
⊢ e = 0
[PROOFSTEP]
have := monoIsKernelOfCokernel _ (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
⊢ e = 0
[PROOFSTEP]
obtain ⟨d, hd⟩ := KernelFork.IsLimit.lift' this u hu
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d :
  R ⟶
    (KernelFork.ofι (biprod.lift f (-g))
        (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0)).pt
hd :
  d ≫
      Fork.ι
        (KernelFork.ofι (biprod.lift f (-g))
          (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0)) =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at d
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd :
  d ≫
      Fork.ι
        (KernelFork.ofι (biprod.lift f (-g))
          (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0)) =
    u
⊢ e = 0
[PROOFSTEP]
dsimp at hd
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
⊢ e = 0
[PROOFSTEP]
have : d ≫ (-g) = 0
[GOAL]
case this
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
⊢ d ≫ (-g) = 0
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this : d ≫ (-g) = 0
⊢ e = 0
[PROOFSTEP]
calc
  d ≫ (-g) = d ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [biprod.lift_snd]
  _ = biprod.lift e (0 : R ⟶ Z) ≫ biprod.snd := by rw [← Category.assoc, hd]
  _ = 0 := biprod.lift_snd _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
⊢ d ≫ (-g) = d ≫ biprod.lift f (-g) ≫ biprod.snd
[PROOFSTEP]
rw [biprod.lift_snd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
⊢ d ≫ biprod.lift f (-g) ≫ biprod.snd = biprod.lift e 0 ≫ biprod.snd
[PROOFSTEP]
rw [← Category.assoc, hd]
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this : d ≫ (-g) = 0
⊢ e = 0
[PROOFSTEP]
have : d = 0 := (cancel_mono (-g)).1 (by simpa)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this : d ≫ (-g) = 0
⊢ d ≫ (-g) = 0 ≫ (-g)
[PROOFSTEP]
simpa
[GOAL]
case mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ e = 0
[PROOFSTEP]
calc
  e = biprod.lift e (0 : R ⟶ Z) ≫ biprod.fst := by rw [biprod.lift_fst]
  _ = (d ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [← hd]
  _ = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst := by rw [this]
  _ = 0 ≫ biprod.lift f (-g) ≫ biprod.fst := by rw [Category.assoc]
  _ = 0 := zero_comp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ e = biprod.lift e 0 ≫ biprod.fst
[PROOFSTEP]
rw [biprod.lift_fst]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ biprod.lift e 0 ≫ biprod.fst = (d ≫ biprod.lift f (-g)) ≫ biprod.fst
[PROOFSTEP]
rw [← hd]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ (d ≫ biprod.lift f (-g)) ≫ biprod.fst = (0 ≫ biprod.lift f (-g)) ≫ biprod.fst
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝¹ :
  IsLimit
    (KernelFork.ofι (biprod.lift f (-g))
      (_ : biprod.lift f (-g) ≫ Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g) = 0))
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this✝ : d ≫ (-g) = 0
this : d = 0
⊢ (0 ≫ biprod.lift f (-g)) ≫ biprod.fst = 0 ≫ biprod.lift f (-g) ≫ biprod.fst
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono (PushoutCocone.inr s)
[PROOFSTEP]
haveI : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.right) := Abelian.mono_pushout_of_mono_f f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono f
s : PushoutCocone f g
hs : IsColimit s
this : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.right)
⊢ Mono (PushoutCocone.inr s)
[PROOFSTEP]
apply mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
s : PushoutCocone f g
hs : IsColimit s
⊢ Mono (PushoutCocone.inl s)
[PROOFSTEP]
haveI : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.left) := Abelian.mono_pushout_of_mono_g f g
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
s : PushoutCocone f g
hs : IsColimit s
this : Mono (NatTrans.app (colimit.cocone (span f g)).ι WalkingCospan.left)
⊢ Mono (PushoutCocone.inl s)
[PROOFSTEP]
apply mono_of_mono_fac (IsColimit.comp_coconePointUniqueUpToIso_hom hs (colimit.isColimit _) _)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasPushouts C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
g₁ : X ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : W ⟶ Y
hf : g₁ ≫ f' = f
t : PushoutCocone f g
ht : IsColimit t
⊢ Mono (PushoutCocone.inl t)
[PROOFSTEP]
apply mono_inl_of_isColimit _ _ (PushoutCocone.isColimitOfFactors _ _ _ _ _ hf hg t ht)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
⊢ {X Y : C} → (f : X ⟶ Y) → [inst : Mono f] → NormalMono f
[PROOFSTEP]
intro _ _ f _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
X✝ Y✝ : C
f : X✝ ⟶ Y✝
inst✝ : Mono f
⊢ NormalMono f
[PROOFSTEP]
convert normalMonoOfMono f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
⊢ {X Y : C} → (f : X ⟶ Y) → [inst : Epi f] → NormalEpi f
[PROOFSTEP]
intro _ _ f _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
X✝ Y✝ : C
f : X✝ ⟶ Y✝
inst✝ : Epi f
⊢ NormalEpi f
[PROOFSTEP]
convert normalEpiOfEpi f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
⊢ HasFiniteProducts C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
⊢ HasKernels C
[PROOFSTEP]
convert (by infer_instance : Limits.HasKernels C)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
⊢ HasKernels C
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
⊢ HasCokernels C
[PROOFSTEP]
convert (by infer_instance : Limits.HasCokernels C)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
src✝ : Preadditive C := preadditive
⊢ HasCokernels C
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom = (λ_ X).hom ⊗ 𝟙 Y
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ ((λ_ X).hom ⊗ 𝟙 Y)
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ 𝟙 X ⊗ (ρ_ Y).inv = (ρ_ (X ⊗ Y)).inv ≫ (α_ X Y tensorUnit').hom
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ X).inv ⊗ 𝟙 Y = (λ_ (X ⊗ Y)).inv ≫ (α_ tensorUnit' X Y).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ 𝟙 Z) ≫ (α_ (W ⊗ X) Y Z).hom = (𝟙 W ⊗ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ ((ρ_ X).inv ⊗ 𝟙 Y) ≫ (α_ X (𝟙_ C) Y).hom = 𝟙 X ⊗ (λ_ Y).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
⊢ (λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) = (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom
[PROOFSTEP]
coherence
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv
[PROOFSTEP]
coherence