awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₁ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (KernelFork.map
      (KernelFork.ofι
        { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom
            { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := kernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C }
            (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) }
        ⋯)
      ShortComplex.π₁)

Tactic:
exact kernelIsKernel _

Premises used: CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₂ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (KernelFork.map
      (KernelFork.ofι
        { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom
            { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := kernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C }
            (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) }
        ⋯)
      ShortComplex.π₂)

Tactic:
exact isLimit f g

Premises used: CategoryTheory.kernelCokernelCompSequence.isLimit
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsLimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₃ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (KernelFork.map
      (KernelFork.ofι
        { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom
            { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := kernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C }
            (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) }
        ⋯)
      ShortComplex.π₃)

Tactic:
exact kernelIsKernel _

Premises used: CategoryTheory.Limits.kernelIsKernel
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₁ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₁)
    (Functor.mapCocone ShortComplex.π₁
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
h₂ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₂)
    (Functor.mapCocone ShortComplex.π₂
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
h₃ :
  IsColimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₃)
    (Functor.mapCocone ShortComplex.π₃
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
⊢ IsColimit (C := ShortComplex.{v, u} C)
    (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)

Tactic:
apply ShortComplex.isColimitOfIsColimitπ

Premises used: CategoryTheory.ShortComplex.isColimitOfIsColimitπ
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₁ :
  IsColimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₁ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (CokernelCofork.map
      (CokernelCofork.ofπ
        { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
            { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := cokernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C } }
        ⋯)
      ShortComplex.π₁)
⊢ IsColimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₁)
    (Functor.mapCocone ShortComplex.π₁
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2

Premises used: CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₂ :
  IsColimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₂ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (CokernelCofork.map
      (CokernelCofork.ofπ
        { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
            { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := cokernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C } }
        ⋯)
      ShortComplex.π₂)
⊢ IsColimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₂)
    (Functor.mapCocone ShortComplex.π₂
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2

Premises used: CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h₃ :
  IsColimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₃ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (CokernelCofork.map
      (CokernelCofork.ofπ
        { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
            { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := cokernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C } }
        ⋯)
      ShortComplex.π₃)
⊢ IsColimit (F :=
    Functor.comp (D := ShortComplex.{v, u} C)
      (parallelPair (X := ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯) (Y :=
        ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
        { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ } 0)
      ShortComplex.π₃)
    (Functor.mapCocone ShortComplex.π₃
      (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))

Tactic:
apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2

Premises used: CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₁ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (CokernelCofork.map
      (CokernelCofork.ofπ
        { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
            { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := cokernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C } }
        ⋯)
      ShortComplex.π₁)

Tactic:
exact cokernelIsCokernel _

Premises used: CategoryTheory.Limits.cokernelIsCokernel
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₂ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (CokernelCofork.map
      (CokernelCofork.ofπ
        { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
            { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := cokernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C } }
        ⋯)
      ShortComplex.π₂)

Tactic:
exact isColimit f g

Premises used: CategoryTheory.kernelCokernelCompSequence.isColimit
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsColimit (F :=
    parallelPair (X :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
      (Y :=
      Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
        (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
      (Functor.map ShortComplex.π₃ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := ⋯, comm₂₃ := ⋯ }) 0)
    (CokernelCofork.map
      (CokernelCofork.ofπ
        { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ :
          ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯)
            { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g ⋯,
              g := cokernel.map (f ≫ g) g f (𝟙 Z) ⋯, zero := ⋯ : ShortComplex.{v, u} C } }
        ⋯)
      ShortComplex.π₃)

Tactic:
exact cokernelIsCokernel _

Premises used: CategoryTheory.Limits.cokernelIsCokernel
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
dsimp : Epi.{v, u} (C := C) (X := biprod.{v, u} X Y) biprod.snd
⊢ Epi.{v, u} (C := C) (X :=
    ShortComplex.X₂.{v, u} (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))
    (ShortComplex.g (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd ⋯))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Epi.{v, u} (C := C) (X := biprod.{v, u} X Y) biprod.snd

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
dsimp : Mono.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl
⊢ Mono.{v, u} (C := C) (X :=
    ShortComplex.X₁.{v, u} (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))
    (ShortComplex.f (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd ⋯))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Mono.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ CategoryStruct.comp (Y := ShortComplex.X₂ (ShortComplex.SnakeInput.L₁ (snakeInput f g))) (kernel.ι g ≫ biprod.inr)
      (ShortComplex.g (ShortComplex.SnakeInput.L₁ (snakeInput f g))) =
    𝟙 (ShortComplex.X₃ (ShortComplex.SnakeInput.L₀ (snakeInput f g))) ≫
      ShortComplex.Hom.τ₃ (ShortComplex.SnakeInput.v₀₁ (snakeInput f g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    ShortComplex.X₃ (ShortComplex.SnakeInput.L₀ (snakeInput f g)) ⟶
      ShortComplex.X₂ (ShortComplex.SnakeInput.L₂ (snakeInput f g)))
    ((-kernel.ι g) ≫ ShortComplex.f (ShortComplex.SnakeInput.L₂ (snakeInput f g)))
    (CategoryStruct.comp (Y := ShortComplex.X₂ (ShortComplex.SnakeInput.L₁ (snakeInput f g))) (kernel.ι g ≫ biprod.inr)
      (ShortComplex.Hom.τ₂ (ShortComplex.SnakeInput.v₁₂ (snakeInput f g))))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := kernel g ⟶ cokernel f) (δ f g) (-kernel.ι g ≫ cokernel.π f)

Tactic:
simpa using (snakeInput f g).δ_eq (𝟙 _) (kernel.ι g ≫ biprod.inr) (-kernel.ι g)
    (by simp) (by aesop)

Premises used: CategoryTheory.kernelCokernelCompSequence.snakeInput, CategoryTheory.CategoryStruct.id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.biprod.inr, CategoryTheory.ShortComplex.SnakeInput.δ_eq, Neg.neg, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
dsimp : Mono (X := kernel f) (Y := kernel (f ≫ g)) (kernel.map f (f ≫ g) (𝟙 X) g ⋯)
⊢ Mono
    ((kernelCokernelCompSequence f g).map' 0 1 instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_2
      instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_4)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Mono (X := kernel f) (Y := kernel (f ≫ g)) (kernel.map f (f ≫ g) (𝟙 X) g ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
dsimp :
  Epi (X :=
    ComposableArrows.Precomp.obj
      (ComposableArrows.mk₄ (X₀ := kernel (f ≫ g)) (X₃ := cokernel (f ≫ g)) (X₄ := cokernel g)
        (kernel.map (f ≫ g) g f (𝟙 Z) ⋯) (δ f g) (cokernel.map f (f ≫ g) (𝟙 X) g ⋯) (cokernel.map (f ≫ g) g f (𝟙 Z) ⋯))
      (kernel f) 4)
    (Y :=
    ComposableArrows.Precomp.obj
      (ComposableArrows.mk₄ (X₀ := kernel (f ≫ g)) (X₃ := cokernel (f ≫ g)) (X₄ := cokernel g)
        (kernel.map (f ≫ g) g f (𝟙 Z) ⋯) (δ f g) (cokernel.map f (f ≫ g) (𝟙 X) g ⋯) (cokernel.map (f ≫ g) g f (𝟙 Z) ⋯))
      (kernel f) 5)
    (cokernel.map (f ≫ g) g f (𝟙 Z) ⋯)
⊢ Epi
    ((kernelCokernelCompSequence f g).map' 4 5 instEpiMap'KernelCokernelCompSequenceOfNatNat._proof_2
      instEpiMap'KernelCokernelCompSequenceOfNatNat._proof_3)

Tactic:
dsimp [ComposableArrows.Precomp.map]

Premises used: CategoryTheory.ComposableArrows.Precomp.map
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Epi (X :=
    ComposableArrows.Precomp.obj
      (ComposableArrows.mk₄ (X₀ := kernel (f ≫ g)) (X₃ := cokernel (f ≫ g)) (X₄ := cokernel g)
        (kernel.map (f ≫ g) g f (𝟙 Z) ⋯) (δ f g) (cokernel.map f (f ≫ g) (𝟙 X) g ⋯) (cokernel.map (f ≫ g) g f (𝟙 Z) ⋯))
      (kernel f) 4)
    (Y :=
    ComposableArrows.Precomp.obj
      (ComposableArrows.mk₄ (X₀ := kernel (f ≫ g)) (X₃ := cokernel (f ≫ g)) (X₄ := cokernel g)
        (kernel.map (f ≫ g) g f (𝟙 Z) ⋯) (δ f g) (cokernel.map f (f ≫ g) (𝟙 X) g ⋯) (cokernel.map (f ≫ g) g f (𝟙 Z) ⋯))
      (kernel f) 5)
    (cokernel.map (f ≫ g) g f (𝟙 Z) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (kernelCokernelCompSequence f g).Exact

Tactic:
(snakeInput f g).snake_lemma

Premises used: CategoryTheory.kernelCokernelCompSequence.snakeInput, CategoryTheory.Limits.colimit, CategoryTheory.Limits.limit, CategoryTheory.ShortComplex.SnakeInput.snake_lemma, CategoryTheory.kernelCokernelCompSequence.δ
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
g : X ⟶ Y
mp :
  epiWithInjectiveKernel g →
    ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g = 0),
      Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
mpr :
  (∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g = 0),
      Nonempty.{v_1 + 1}
        { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.Splitting) →
    epiWithInjectiveKernel g
⊢ epiWithInjectiveKernel g ↔
    ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g = 0),
      Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
g : X ⟶ Y
left : Epi g
right : Injective.{v_1, u_1} (kernel g)
⊢ Eq (α := kernel g ⟶ Y) (kernel.ι g ≫ g) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
g : X ⟶ Y
left : Epi g
right : Injective.{v_1, u_1} (kernel g)
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := kernel g) (kernel.ι g) g ⋯
⊢ S.f ≫ Injective.factorThru (𝟙 S.X₁) (kernel.ι g) = 𝟙 S.X₁

Tactic:
simp [S]
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
g : X ⟶ Y
left : Epi g
right : Injective.{v_1, u_1} (kernel g)
S : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := kernel g) (kernel.ι g) g ⋯
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
exact ⟨_, inferInstance, _, S.zero,
      ⟨ShortComplex.Splitting.ofExactOfRetraction S
        (S.exact_of_f_is_kernel (kernelIsKernel g)) (Injective.factorThru (𝟙 _) (kernel.ι g))
        (by simp [S]) inferInstance⟩⟩
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
g : X ⟶ Y
I : C
w_1 : Injective.{v_1, u_1} I
f : I ⟶ X
w : f ≫ g = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
⊢ IsSplitEpi g

Tactic:
have : IsSplitEpi g := ⟨σ.s, σ.s_g⟩
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
g : X ⟶ Y
I : C
w_1 : Injective.{v_1, u_1} I
f : I ⟶ X
w : f ≫ g = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
this : IsSplitEpi g
e : I ≅ kernel g :=
  ⋯.fIsKernel.conePointUniqueUpToIso
    (limit.isLimit
      (parallelPair { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.g 0))
⊢ epiWithInjectiveKernel g

Tactic:
⟨inferInstance, Injective.of_iso e inferInstance⟩

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel, CategoryTheory.Injective.of_iso, inferInstance, And.intro