awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 :=
    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.mapCone ShortComplex.π₂
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
have h₂ : 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 sorry))
    (Y :=
    Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
      (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry))
    (Functor.map ShortComplex.π₂ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry }) 0)
  (KernelFork.map
    (KernelFork.ofι
      { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := sorry, comm₂₃ := sorry :
        ShortComplex.Hom
          { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g sorry,
            g := kernel.map (f ≫ g) g f (𝟙 Z) sorry, zero := sorry : ShortComplex.{v, u} C }
          (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd sorry) }
      sorry)
    ShortComplex.π₂)
Tactic: apply (KernelFork.isLimitMapConeEquiv _ _).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 :=
    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.mapCone ShortComplex.π₃
      (KernelFork.ofι { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯))
have h₃ : 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 sorry))
    (Y :=
    Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
      (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry))
    (Functor.map ShortComplex.π₃ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry }) 0)
  (KernelFork.map
    (KernelFork.ofι
      { τ₁ := kernel.ι f, τ₂ := ι f g, τ₃ := kernel.ι g, comm₁₂ := sorry, comm₂₃ := sorry :
        ShortComplex.Hom
          { X₁ := kernel f, X₂ := kernel (f ≫ g), X₃ := kernel g, f := kernel.map f (f ≫ g) (𝟙 X) g sorry,
            g := kernel.map (f ≫ g) g f (𝟙 Z) sorry, zero := sorry : ShortComplex.{v, u} C }
          (ShortComplex.mk (X₁ := X) (X₂ := biprod.{v, u} X Y) biprod.inl biprod.snd sorry) }
      sorry)
    ShortComplex.π₃)
Tactic: apply (KernelFork.isLimitMapConeEquiv _ _).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 (C := ShortComplex.{v, u} C)
    (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)
have 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 sorry) (Y :=
      ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry)
      { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry } 0)
    ShortComplex.π₁)
  (Functor.mapCocone ShortComplex.π₁
    (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := sorry, comm₂₃ := sorry } sorry))
Tactic: apply ShortComplex.isColimitOfIsColimitπ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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₂₃ := ⋯ } ⋯))
⊢ IsColimit (C := ShortComplex.{v, u} C)
    (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)
have 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 sorry) (Y :=
      ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry)
      { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry } 0)
    ShortComplex.π₂)
  (Functor.mapCocone ShortComplex.π₂
    (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := sorry, comm₂₃ := sorry } sorry))
Tactic: apply ShortComplex.isColimitOfIsColimitπ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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₂₃ := ⋯ } ⋯))
⊢ IsColimit (C := ShortComplex.{v, u} C)
    (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := ⋯, comm₂₃ := ⋯ } ⋯)
have 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 sorry) (Y :=
      ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry)
      { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry } 0)
    ShortComplex.π₃)
  (Functor.mapCocone ShortComplex.π₃
    (CokernelCofork.ofπ { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := sorry, comm₂₃ := sorry } sorry))
Tactic: apply ShortComplex.isColimitOfIsColimitπ
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 :=
    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₂₃ := ⋯ } ⋯))
have 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 sorry))
    (Y :=
    Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₁
      (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry))
    (Functor.map ShortComplex.π₁ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry }) 0)
  (CokernelCofork.map
    (CokernelCofork.ofπ
      { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := sorry, comm₂₃ := sorry :
        ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry)
          { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g sorry,
            g := cokernel.map (f ≫ g) g f (𝟙 Z) sorry, zero := sorry : ShortComplex.{v, u} C } }
      sorry)
    ShortComplex.π₁)
Tactic: apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 :=
    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₂₃ := ⋯ } ⋯))
have 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 sorry))
    (Y :=
    Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₂
      (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry))
    (Functor.map ShortComplex.π₂ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry }) 0)
  (CokernelCofork.map
    (CokernelCofork.ofπ
      { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := sorry, comm₂₃ := sorry :
        ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry)
          { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g sorry,
            g := cokernel.map (f ≫ g) g f (𝟙 Z) sorry, zero := sorry : ShortComplex.{v, u} C } }
      sorry)
    ShortComplex.π₂)
Tactic: apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 :=
    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₂₃ := ⋯ } ⋯))
have 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 sorry))
    (Y :=
    Functor.obj (C := ShortComplex.{v, u} C) ShortComplex.π₃
      (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry))
    (Functor.map ShortComplex.π₃ { τ₁ := f, τ₂ := φ f g, τ₃ := g, comm₁₂ := sorry, comm₂₃ := sorry }) 0)
  (CokernelCofork.map
    (CokernelCofork.ofπ
      { τ₁ := cokernel.π f, τ₂ := π f g, τ₃ := cokernel.π g, comm₁₂ := sorry, comm₂₃ := sorry :
        ShortComplex.Hom (ShortComplex.mk (X₁ := Y) (X₂ := biprod.{v, u} Y Z) biprod.inl biprod.snd sorry)
          { X₁ := cokernel f, X₂ := cokernel (f ≫ g), X₃ := cokernel g, f := cokernel.map f (f ≫ g) (𝟙 X) g sorry,
            g := cokernel.map (f ≫ g) g f (𝟙 Z) sorry, zero := sorry : ShortComplex.{v, u} C } }
      sorry)
    ShortComplex.π₃)
Tactic: apply (CokernelCofork.isColimitMapCoconeEquiv _ _).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 :=
    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 ⋯))
have dsimp : Epi.{v, u} (C := C) (X := biprod.{v, u} X Y) biprod.snd
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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 :=
    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 ⋯))
have dsimp : Mono.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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
    ((kernelCokernelCompSequence f g).map' 0 1 instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_2
      instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_4)
have dsimp : Mono (X := kernel f) (Y := kernel (f ≫ g)) (kernel.map f (f ≫ g) (𝟙 X) g sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp (goal)
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
    ((kernelCokernelCompSequence f g).map' 4 5 instEpiMap'KernelCokernelCompSequenceOfNatNat._proof_2
      instEpiMap'KernelCokernelCompSequenceOfNatNat._proof_3)
have 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) sorry) (δ f g) (cokernel.map f (f ≫ g) (𝟙 X) g sorry) (cokernel.map (f ≫ g) g f (𝟙 Z) sorry))
    (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) sorry) (δ f g) (cokernel.map f (f ≫ g) (𝟙 X) g sorry) (cokernel.map (f ≫ g) g f (𝟙 Z) sorry))
    (kernel f) 5)
  (cokernel.map (f ≫ g) g f (𝟙 Z) sorry)
Tactic: dsimp [ComposableArrows.Precomp.map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (hypothesis)
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
⊢ epiWithInjectiveKernel g
have this : IsSplitEpi g
Tactic: have : IsSplitEpi g := ⟨σ.s, σ.s_g⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ epiWithInjectiveKernel f
have rw : ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f_1 : I ⟶ X) (w : f_1 ≫ f = 0),
  Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f_1, g := f, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
Tactic: rw [epiWithInjectiveKernel_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hY : IsZero.{v_1, u_1} Y
⊢ epiWithInjectiveKernel f ↔ Injective.{v_1, u_1} X
have simp : Injective.{v_1, u_1} (kernel f) ↔ Injective.{v_1, u_1} X
Tactic: simp only [epiWithInjectiveKernel, hY.epi f, true_and]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
hg₁ : epiWithInjectiveKernel g₁
hg₂ : epiWithInjectiveKernel g₂
⊢ epiWithInjectiveKernel (g₁ ≫ g₂)
have rw : ∀
  (hg₁ :
    ∃ (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)
  (hg₂ :
    ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ Y) (w : f ≫ g₂ = 0),
      Nonempty.{v_1 + 1}
        { X₁ := I, X₂ := Y, X₃ := Z, f := f, g := g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting),
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
Tactic: rw [epiWithInjectiveKernel_iff] at hg₁ hg₂ ⊢
Cleared hypotheses: hg₁, hg₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
hg₁ :
  ∃ (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
hg₂ :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ Y) (w : f ≫ g₂ = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := Y, X₃ := Z, f := f, g := g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have obtain : ∀ (I₁ : C),
  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),
      ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
        Nonempty.{v_1 + 1}
          { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
Tactic: obtain ⟨I₁, _, f₁, w₁, ⟨σ₁⟩⟩ := hg₁
Cleared hypotheses: hg₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
hg₂ :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ Y) (w : f ≫ g₂ = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := Y, X₃ := Z, f := f, g := g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
I₁ : C
w : 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
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have obtain : ∀ (I₂ : C),
  Injective.{v_1, u_1} I₂ →
    ∀ (f₂ : I₂ ⟶ Y) (w₂ : f₂ ≫ g₂ = 0)
      (σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting),
      ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
        Nonempty.{v_1 + 1}
          { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
Tactic: obtain ⟨I₂, _, f₂, w₂, ⟨σ₂⟩⟩ := hg₂
Cleared hypotheses: hg₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : 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
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have refine_1 : HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = 0
Tactic: refine ⟨I₁ ⊞ I₂, inferInstance, biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, ?_, ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : 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
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
refine_1 : HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = 0
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
have refine_2 : { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
    f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
    zero := sorry : ShortComplex.{v_1, u_1} C }.Splitting
Tactic: refine ⟨I₁ ⊞ I₂, inferInstance, biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, ?_, ⟨?_⟩⟩