awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
X : C
P : ProjectiveResolution.{v, u} X
rw :
  Nonempty
    (IsColimit (F :=
      parallelPair (X :=
        ShortComplex.X₁
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        (ShortComplex.f
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        0)
      (CokernelCofork.ofπ
        (ShortComplex.g
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        ⋯))
⊢ IsIso (X := HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
    (HomologicalComplex.descOpcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)
        (F.map (P.π.f 0)) 1 ProjectiveResolution.fromLeftDerivedZero'._proof_1 ⋯ :
      HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)

Tactic:
rw [ChainComplex.isIso_descOpcycles_iff, ShortComplex.exact_and_epi_g_iff_g_is_cokernel]

Premises used: ChainComplex.isIso_descOpcycles_iff, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
X : C
P : ProjectiveResolution.{v, u} X
⊢ Nonempty
    (IsColimit (F :=
      parallelPair (X :=
        ShortComplex.X₁
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        (ShortComplex.f
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        0)
      (CokernelCofork.ofπ
        (ShortComplex.g
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        ⋯))

Tactic:
⟨CokernelCofork.mapIsColimit _ (P.isColimitCokernelCofork) F⟩

Premises used: Nonempty.intro, CategoryTheory.ProjectiveResolution.isColimitCokernelCofork, CategoryTheory.Limits.CokernelCofork.mapIsColimit
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
X : C
P : ProjectiveResolution.{v, u} X
⊢ Nonempty
    (IsColimit (F :=
      parallelPair (X :=
        ShortComplex.X₁
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        (ShortComplex.f
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        0)
      (CokernelCofork.ofπ
        (ShortComplex.g
          (ShortComplex.mk (X₁ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1) (X₂ :=
            HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0 :
              HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶
                HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
            (F.map (P.π.f 0) : F.obj (P.complex.X 0) ⟶ F.obj X) ⋯))
        ⋯))

Tactic:
exact ⟨CokernelCofork.mapIsColimit _ (P.isColimitCokernelCofork) F⟩
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
X : C
dsimp :
  IsIso (X := (F.leftDerived 0).obj X)
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))) ≫
        HomologicalComplex.homologyι
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X)))
            0 ≫
          ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution X) F :
      (F.leftDerived 0).obj X ⟶ F.obj X)
⊢ IsIso (X := (F.leftDerived 0).obj X) (NatTrans.app F.fromLeftDerivedZero X)

Tactic:
dsimp [Functor.fromLeftDerivedZero]

Premises used: CategoryTheory.Functor.fromLeftDerivedZero
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
X : C
⊢ IsIso (X := (F.leftDerived 0).obj X)
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))) ≫
        HomologicalComplex.homologyι
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X)))
            0 ≫
          ProjectiveResolution.fromLeftDerivedZero' (projectiveResolution X) F :
      (F.leftDerived 0).obj X ⟶ F.obj X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
⊢ IsIso (X := F.leftDerived 0) F.fromLeftDerivedZero

Tactic:
NatIso.isIso_of_isIso_app _

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
⊢ F.fromLeftDerivedZero ≫ Iso.inv F.leftDerivedZeroIsoSelf = 𝟙 (F.leftDerived 0)

Tactic:
F.leftDerivedZeroIsoSelf.hom_inv_id

Premises used: CategoryTheory.Functor.leftDerivedZeroIsoSelf, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.fromLeftDerivedZero
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
⊢ CategoryStruct.comp (Y := F.leftDerived 0) (Iso.inv F.leftDerivedZeroIsoSelf) F.fromLeftDerivedZero = 𝟙 F

Tactic:
F.leftDerivedZeroIsoSelf.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.leftDerivedZeroIsoSelf, CategoryTheory.Functor.fromLeftDerivedZero
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
X : C
⊢ NatTrans.app F.fromLeftDerivedZero X ≫ NatTrans.app (Iso.inv F.leftDerivedZeroIsoSelf) X = 𝟙 ((F.leftDerived 0).obj X)

Tactic:
F.leftDerivedZeroIsoSelf.hom_inv_id_app X

Premises used: CategoryTheory.Functor.leftDerivedZeroIsoSelf, CategoryTheory.Iso.hom_inv_id_app
-- Module: Mathlib.CategoryTheory.Abelian.LeftDerived
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
inst_6 : PreservesFiniteColimits F
X : C
⊢ CategoryStruct.comp (Y := (F.leftDerived 0).obj X) (NatTrans.app (Iso.inv F.leftDerivedZeroIsoSelf) X)
      (NatTrans.app F.fromLeftDerivedZero X) =
    𝟙 (F.obj X)

Tactic:
F.leftDerivedZeroIsoSelf.inv_hom_id_app X

Premises used: CategoryTheory.Functor.leftDerivedZeroIsoSelf, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Abelian.Monomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
x x_1 x_2 : C
f : x ⟶ x_2
g : x ⟶ x_1
h : Limits.HasPushout f g
hf : monomorphisms C f
⊢ Mono f

Tactic:
simp only [monomorphisms.iff] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.monomorphisms.iff
-- Module: Mathlib.CategoryTheory.Abelian.Monomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
x x_1 x_2 : C
f : x ⟶ x_2
g : x ⟶ x_1
h : Limits.HasPushout f g
hf : Mono f
⊢ Mono (Y := Limits.pushout f g) (Limits.pushout.inr f g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Monomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
x x_1 x_2 : C
f : x ⟶ x_2
g : x_1 ⟶ x_2
h : Limits.HasPullback f g
hf : epimorphisms C g
⊢ Epi g

Tactic:
simp only [epimorphisms.iff] at hf ⊢

Premises used: CategoryTheory.MorphismProperty.epimorphisms.iff
-- Module: Mathlib.CategoryTheory.Abelian.Monomorphisms
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
x x_1 x_2 : C
f : x ⟶ x_2
g : x_1 ⟶ x_2
h : Limits.HasPullback f g
hf : Epi g
⊢ Epi (X := Limits.pullback f g) (Limits.pullback.fst f g)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
haveI : ∀ (hu : NormalMono u), g = 0
⊢ g = 0

Tactic:
haveI hu := normalMonoOfMono u
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
obtain : ∀ (t : P ⟶ kernel g) (ht : t ≫ kernel.ι g = p), g = 0
⊢ g = 0

Tactic:
obtain ⟨t, ht⟩ := kernel.lift' g p hpg

Premises used: CategoryTheory.Limits.kernel.lift'
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
⊢ ((t ≫ kernel.ι g) ≫ i) ≫ h = t ≫ u ≫ h

Tactic:
simp only [u, Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
⊢ f ≫ h = 0

Tactic:
have fh : f ≫ h = 0 :=
    calc
      f ≫ h = (p ≫ i) ≫ h := (Abelian.image.fac f).symm ▸ rfl
      _ = ((t ≫ kernel.ι g) ≫ i) ≫ h := ht ▸ rfl
      _ = t ≫ u ≫ h := by simp only [u, Category.assoc]
      _ = t ≫ 0 := hu.w ▸ rfl
      _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
obtain : ∀ (l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _) (hl : cokernel.π f ≫ l = h), g = 0
⊢ g = 0

Tactic:
obtain ⟨l, hl⟩ := cokernel.desc' f h fh

Premises used: CategoryTheory.Limits.cokernel.desc'
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _
hl : cokernel.π f ≫ l = h
rw : (i ≫ cokernel.π f) ≫ l = 0 ≫ l
rw₁ rw₂ :
  Eq (α := kernel (Y := cokernel f) (cokernel.π f) ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _) (0 ≫ l) (0 ≫ l)
⊢ i ≫ cokernel.π f ≫ l = 0 ≫ l

Tactic:
rw [← Category.assoc, kernel.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.kernel.condition
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _
hl : cokernel.π f ≫ l = h
⊢ i ≫ h = 0

Tactic:
have hih : i ≫ h = 0 :=
    calc
      i ≫ h = i ≫ cokernel.π f ≫ l := hl ▸ rfl
      _ = 0 ≫ l := by rw [← Category.assoc, kernel.condition]
      _ = 0 := zero_comp
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
obtain : ∀ (s : kernel (Y := cokernel f) (cokernel.π f) ⟶ kernel g) (hs : s ≫ u = i), g = 0
⊢ g = 0

Tactic:
obtain ⟨s, hs⟩ := NormalMono.lift' u i hih

Premises used: CategoryTheory.NormalMono.lift'
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (Y := cokernel f) (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
rw : s ≫ kernel.ι g ≫ i = 𝟙 I ≫ i
rw₁ : i = 𝟙 I ≫ i
rw₂ rw₃ : i = i
⊢ (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i

Tactic:
rw [Category.assoc, hs, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (Y := cokernel f) (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
⊢ (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i

Tactic:
have hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i := by rw [Category.assoc, hs, Category.id_comp]
-- Module: Mathlib.CategoryTheory.Abelian.NonPreadditive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : NonPreadditiveAbelian.{v, u} C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (Y := cokernel f) (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _ := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (Y := cokernel f) (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i
⊢ Epi (X := kernel g) (kernel.ι g)

Tactic:
haveI : Epi (kernel.ι g) := epi_of_epi_fac ((cancel_mono _).1 hs')