awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α := HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0)
      (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 0)
      (F.map (P.π.f 0)))
    0
have dsimp : Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
  (CategoryStruct.comp (Y := F.obj (P.complex.X 0)) (F.map (P.complex.d 1 0)) (F.map (P.π.f 0)) :
    F.obj (P.complex.X 1) ⟶ F.obj X)
  (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (P.complex.X 0)) (F.map (P.complex.d 1 0)) (F.map (P.π.f 0)) :
      F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
have rw : Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
  (F.map (CategoryStruct.comp (Y := P.complex.X 0) (P.complex.d 1 0) (P.π.f 0)) : F.obj (P.complex.X 1) ⟶ F.obj X)
  (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
Tactic: rw [← F.map_comp, complex_d_comp_π_f_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
rw :
  Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (F.map (CategoryStruct.comp (Y := P.complex.X 0) (P.complex.d 1 0) (P.π.f 0)) : F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
⊢ Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (P.complex.X 0)) (F.map (P.complex.d 1 0)) (F.map (P.π.f 0)) :
      F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
have rw₁ : Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X) (F.map 0) 0
Tactic: rw [← F.map_comp, complex_d_comp_π_f_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
rw :
  Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (F.map (CategoryStruct.comp (Y := P.complex.X 0) (P.complex.d 1 0) (P.π.f 0)) : F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
rw₁ : Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X) (F.map 0) 0
⊢ Eq (α := F.obj (P.complex.X 1) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (P.complex.X 0)) (F.map (P.complex.d 1 0)) (F.map (P.π.f 0)) :
      F.obj (P.complex.X 1) ⟶ F.obj X)
    (0 : HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 1 ⟶ F.obj X)
have rw₂ : Eq.{v_1 + 1} (α := F.obj (P.complex.X 1) ⟶ F.obj X) 0 0
Tactic: rw [← F.map_comp, complex_d_comp_π_f_zero, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
inst_6 : Projective.{v, u} X
⊢ IsIso (X :=
    HomologicalComplex.opcycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (self X)))
      0)
    (fromLeftDerivedZero' (self X) F :
      HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (self X)))
          0 ⟶
        F.obj X)
have dsimp : IsIso (X :=
  HomologicalComplex.opcycles
    (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
      (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
    0)
  (HomologicalComplex.descOpcycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
      (F.map (𝟙 X)) 1 fromLeftDerivedZero'._proof_1 sorry :
    HomologicalComplex.opcycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        0 ⟶
      F.obj X)
Tactic: dsimp [ProjectiveResolution.fromLeftDerivedZero']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
inst_6 : Projective.{v, u} X
⊢ IsIso (X :=
    HomologicalComplex.opcycles
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
      0)
    (HomologicalComplex.descOpcycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        (F.map (𝟙 X)) 1 fromLeftDerivedZero'._proof_1 ⋯ :
      HomologicalComplex.opcycles
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          0 ⟶
        F.obj X)
have rw : ShortComplex.Exact
    (ShortComplex.mk (X₁ :=
      HomologicalComplex.X
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        1)
      (HomologicalComplex.d
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
        1 0)
      (F.map (𝟙 X)) sorry) ∧
  Epi (F.map (𝟙 X))
Tactic: rw [ChainComplex.isIso_descOpcycles_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
inst_6 : Projective.{v, u} X
⊢ ShortComplex.Exact
      (ShortComplex.mk (X₁ :=
        HomologicalComplex.X
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1)
        (HomologicalComplex.d
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
          1 0)
        (F.map (𝟙 X)) ⋯) ∧
    Epi (F.map (𝟙 X))
have refine : ShortComplex.Splitting
  (ShortComplex.mk (X₁ :=
    HomologicalComplex.X
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
      1)
    (HomologicalComplex.d
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (Functor.obj (ChainComplex.single₀ C) X))
      1 0)
    (F.map (𝟙 X)) sorry)
Tactic: refine ⟨ShortComplex.Splitting.exact ?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α := (F.leftDerived 0).obj X ⟶ F.obj X) (NatTrans.app F.fromLeftDerivedZero X)
    (Iso.hom (P.isoLeftDerivedObj F 0) ≫
      Iso.hom (ChainComplex.isoHomologyι₀ (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
        P.fromLeftDerivedZero' F)
have dsimp : Eq (α := (F.leftDerived 0).obj X ⟶ F.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 ≫
        fromLeftDerivedZero' (projectiveResolution X) F :
    (F.leftDerived 0).obj X ⟶ F.obj X)
  ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
          (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
        NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
      HomologicalComplex.homologyι (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ≫
        P.fromLeftDerivedZero' F :
    (F.leftDerived 0).obj X ⟶ F.obj X)
Tactic: dsimp [Functor.fromLeftDerivedZero, isoLeftDerivedObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
X : C
inst_6 : Projective.{v, u} X
⊢ IsIso (X := (F.leftDerived 0).obj X) (NatTrans.app F.fromLeftDerivedZero X)
have rw : IsIso (X := (F.leftDerived 0).obj X)
  (CategoryStruct.comp (Y :=
    Functor.obj (C := HomologicalComplex.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) 0)
      (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
        (F.mapHomologicalComplex (ComplexShape.down ℕ)) (ProjectiveResolution.complex (ProjectiveResolution.self X))))
    (Iso.hom (ProjectiveResolution.isoLeftDerivedObj (ProjectiveResolution.self X) F 0))
    (Iso.hom
        (ChainComplex.isoHomologyι₀
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (ProjectiveResolution.complex (ProjectiveResolution.self X)))) ≫
      ProjectiveResolution.fromLeftDerivedZero' (ProjectiveResolution.self X) F))
Tactic: rw [(ProjectiveResolution.self X).fromLeftDerivedZero_eq F]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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
⊢ 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)
have 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) sorry))
      (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) sorry))
      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) sorry))
      sorry))
Tactic: rw [ChainComplex.isIso_descOpcycles_iff, ShortComplex.exact_and_epi_g_iff_g_is_cokernel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
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 F.fromLeftDerivedZero X)
have 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)
Tactic: dsimp [Functor.fromLeftDerivedZero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Monomorphisms (hypothesis)
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
⊢ monomorphisms C (Y := Limits.pushout f g) (Limits.pushout.inr f g)
have hf₁ : Mono f
Tactic: simp only [monomorphisms.iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Monomorphisms (hypothesis)
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
⊢ epimorphisms C (X := Limits.pullback f g) (Limits.pullback.fst f g)
have hf₁ : Epi g
Tactic: simp only [epimorphisms.iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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
⊢ g = 0
have haveI : ∀ (hu : NormalMono u), g = 0
Tactic: haveI hu := normalMonoOfMono u
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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
⊢ g = 0
have obtain : ∀ (t : P ⟶ kernel g) (ht : t ≫ kernel.ι g = p), g = 0
Tactic: obtain ⟨t, ht⟩ := kernel.lift' g p hpg
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (hypothesis)
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
⊢ g = 0
have fh : 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 _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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
⊢ g = 0
have obtain : ∀ (l : cokernel f ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _) (hl : cokernel.π f ≫ l = h), g = 0
Tactic: obtain ⟨l, hl⟩ := cokernel.desc' f h fh
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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 ≫ cokernel.π f ≫ l = 0 ≫ l
have rw : (i ≫ cokernel.π f) ≫ l = 0 ≫ l
Tactic: rw [← Category.assoc, kernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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
⊢ i ≫ cokernel.π f ≫ l = 0 ≫ l
have rw₁ : Eq (α := kernel (Y := cokernel f) (cokernel.π f) ⟶ @NormalMono.Z _ _ _ _ toHasZeroMorphisms u _) (0 ≫ l) (0 ≫ l)
Tactic: rw [← Category.assoc, kernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (hypothesis)
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
⊢ g = 0
have hih : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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
⊢ g = 0
have obtain : ∀ (s : kernel (Y := cokernel f) (cokernel.π f) ⟶ kernel g) (hs : s ≫ u = i), g = 0
Tactic: obtain ⟨s, hs⟩ := NormalMono.lift' u i hih
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.NonPreadditive (goal)
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
have rw : s ≫ kernel.ι g ≫ i = 𝟙 I ≫ i
Tactic: rw [Category.assoc, hs, Category.id_comp]