awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B) (S.map L)
  ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L) :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (ShortComplex.X₂ (S.map L)), τ₃ := 𝟙 (ShortComplex.X₃ (S.map L)),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ShortComplex.Exact (S.map L)
have hL : ShortComplex.Exact
  ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := sorry :
        ShortComplex.{v₁, u₁} A }.map
    L)
Tactic: apply (ShortComplex.exact_iff_of_epi_of_isIso_of_mono φ).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Exact (goal)
Goal:
A : Type u₁
B : Type u₂
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Abelian.{v₁, u₁} A
inst_3 : Abelian.{v₂, u₂} B
L : Functor.{v₁, v₂, u₁, u₂} A B
inst_4 : L.PreservesZeroMorphisms
inst_5 : L.PreservesEpimorphisms
inst_6 : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex.{v₁, u₁} A
hS : S.Exact
φ : Quiver.Hom (V := ShortComplex.{v₂, u₂} B) (S.map L)
  ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
        ShortComplex.{v₁, u₁} A }.map
    L) :=
  { τ₁ := L.map (Abelian.factorThruImage S.f), τ₂ := 𝟙 (ShortComplex.X₂ (S.map L)), τ₃ := 𝟙 (ShortComplex.X₃ (S.map L)),
    comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ShortComplex.Exact
    ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := ⋯ :
          ShortComplex.{v₁, u₁} A }.map
      L)
have hL : IsLimit (F :=
  parallelPair (X :=
    ShortComplex.X₂
      ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := sorry :
            ShortComplex.{v₁, u₁} A }.map
        L))
    (ShortComplex.g
      ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := sorry :
            ShortComplex.{v₁, u₁} A }.map
        L))
    0)
  (KernelFork.ofι
    (ShortComplex.f
      ({ X₁ := Abelian.image S.f, X₂ := S.X₂, X₃ := S.X₃, f := Abelian.image.ι S.f, g := S.g, zero := sorry :
            ShortComplex.{v₁, u₁} A }.map
        L))
    sorry)
Tactic: apply ShortComplex.exact_of_f_is_kernel
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Ext (goal)
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ IsZero (C := ModuleCat.{v_1, u_1} R) (Functor.obj (Functor.obj (Ext R C (n + 1)) (Opposite.op X)) Y)
have refine : IsZero (C := ModuleCat.{v_1, u_1} R)
  (HomologicalComplex.homology
    (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))
Tactic: refine IsZero.of_iso ?_ ((ProjectiveResolution.self X).isoExt (n + 1) Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Ext (goal)
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ IsZero (C := ModuleCat.{v_1, u_1} R)
    (HomologicalComplex.homology
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))
have rw : ShortComplex.Exact (C := ModuleCat.{v_1, u_1} R)
  (HomologicalComplex.sc (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y)
    (n + 1))
Tactic: rw [← HomologicalComplex.exactAt_iff_isZero_homology, HomologicalComplex.exactAt_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Ext (goal)
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ ShortComplex.Exact (C := ModuleCat.{v_1, u_1} R)
    (HomologicalComplex.sc
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1))
have refine : IsZero (C := ModuleCat.{v_1, u_1} R)
  (ShortComplex.X₂
    (HomologicalComplex.sc
      (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1)))
Tactic: refine ShortComplex.exact_of_isZero_X₂ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Ext (goal)
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ IsZero (C := ModuleCat.{v_1, u_1} R)
    (ShortComplex.X₂
      (HomologicalComplex.sc
        (ChainComplex.linearYonedaObj (ProjectiveResolution.complex (ProjectiveResolution.self X)) R Y) (n + 1)))
have dsimp : IsZero (C := ModuleCat.{v_1, u_1} R)
  (Functor.obj (Functor.obj (linearYoneda R C) Y)
    (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Ext (goal)
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ IsZero (C := ModuleCat.{v_1, u_1} R)
    (Functor.obj (Functor.obj (linearYoneda R C) Y)
      (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))
have rw : Eq.{v_1 + 1} (α :=
  Quiver.Hom (V := ModuleCat.{v_1, u_1} R)
    (Functor.obj (Functor.obj (linearYoneda R C) Y)
      (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))
    (Functor.obj (Functor.obj (linearYoneda R C) Y)
      (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
  (𝟙
    (Functor.obj (Functor.obj (linearYoneda R C) Y)
      (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
  0
Tactic: rw [IsZero.iff_id_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Ext (goal)
Goal:
R : Type u_1
inst : Ring R
C : Type u_2
inst_1 : Category.{v_1, u_2} C
inst_2 : Abelian.{v_1, u_2} C
inst_3 : Linear.{u_1, v_1, u_2} R C
inst_4 : EnoughProjectives.{v_1, u_2} C
X Y : C
inst_5 : Projective.{v_1, u_2} X
n : ℕ
⊢ Eq.{v_1 + 1} (α :=
    Quiver.Hom (V := ModuleCat.{v_1, u_1} R)
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
    (𝟙
      (Functor.obj (Functor.obj (linearYoneda R C) Y)
        (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))))
    0
have hf : ∀
  (x :
    Opposite.unop (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))) ⟶
      Y),
  Eq (α :=
    (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
          (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
      Type v_1))
    ((ModuleCat.Hom.hom
            (𝟙
              (Functor.obj (Functor.obj (linearYoneda R C) Y)
                (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1))))) :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        x :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))
    ((ModuleCat.Hom.hom 0 :
          (a :
              (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) :
                Type v_1)) →
            (↑(((linearYoneda R C).obj Y).obj (Opposite.op (((ChainComplex.single₀ C).obj X).X (n + 1)))) : Type v_1))
        x :
      (↑(Functor.obj (Functor.obj (linearYoneda R C) Y)
            (Opposite.op (HomologicalComplex.X.{v_1, u_2, 0} (Functor.obj (ChainComplex.single₀ C) X) (n + 1)))) :
        Type v_1))
Tactic: ext (x : _ ⟶ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Functor.Faithful (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this : Functor.Faithful (F C)
Tactic: have : (F C).Faithful := by rw [F]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : Functor.Faithful (F C)
⊢ Functor.Faithful (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : Functor.Faithful (C := AsSmall C) (G C)
Tactic: have : (G C).Faithful := by rw [G]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : Functor.Faithful (F C)
this : Functor.Faithful (C := AsSmall C) (G C)
⊢ Functor.Faithful (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : Functor.Faithful (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)
Tactic: have : (H C).Faithful := IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Functor.Full (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this : Functor.Full (F C)
Tactic: have : (F C).Full := by rw [F]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : Functor.Full (F C)
⊢ Functor.Full (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : Functor.Full (C := AsSmall C) (G C)
Tactic: have : (G C).Full := by rw [G]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : Functor.Full (F C)
this : Functor.Full (C := AsSmall C) (G C)
⊢ Functor.Full (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : Functor.Full (C := AsSmall C) (D := ModuleCat (EmbeddingRing.{v, u} C)) (G C ⋙ H C)
Tactic: have : (G C ⋙ H C).Full := IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ PreservesFiniteLimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this : PreservesFiniteLimits (F C)
Tactic: have : PreservesFiniteLimits (F C) := by rw [F]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : PreservesFiniteLimits (F C)
⊢ PreservesFiniteLimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : PreservesFiniteLimits (C := AsSmall C) (G C)
Tactic: have : PreservesFiniteLimits (G C) := by rw [G]; apply preservesFiniteLimits_rightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : PreservesFiniteLimits (F C)
this : PreservesFiniteLimits (C := AsSmall C) (G C)
⊢ PreservesFiniteLimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : PreservesFiniteLimits (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)
Tactic: have : PreservesFiniteLimits (H C) :=
    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ PreservesFiniteColimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this : PreservesFiniteColimits (F C)
Tactic: have : PreservesFiniteColimits (F C) := by rw [F]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : PreservesFiniteColimits (F C)
⊢ PreservesFiniteColimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : PreservesFiniteColimits (C := AsSmall C) (G C)
Tactic: have : PreservesFiniteColimits (G C) := by rw [G]; apply preservesFiniteColimits_rightOp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FreydMitchell (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : PreservesFiniteColimits (F C)
this : PreservesFiniteColimits (C := AsSmall C) (G C)
⊢ PreservesFiniteColimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)
have this₁ : PreservesFiniteColimits (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)
Tactic: have : PreservesFiniteColimits (H C) :=
    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := Functor.obj (Functor.obj (evaluation C D) X) (kernel α) ⟶ F.obj X)
    (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι α) ≫
      Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) F)))
    (CategoryStruct.comp (Y := kernel (α.app X)) (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) α))
      (kernel.ι (α.app X)))
have dsimp : Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X ≫ 𝟙 (F.obj X))
  (CategoryStruct.comp (Y := kernel (α.app X)) (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) α))
    (kernel.ι (α.app X)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X ≫ 𝟙 (F.obj X))
    (CategoryStruct.comp (Y := kernel (α.app X)) (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) α))
      (kernel.ι (α.app X)))
have simp : Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X)
  (CategoryStruct.comp (Y := kernel (α.app X)) (kernelComparison α (Functor.obj (evaluation C D) X))
    (kernel.ι (α.app X)))
Tactic: simp only [Category.comp_id, PreservesKernel.iso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := Functor.obj (Functor.obj (evaluation C D) X) G ⟶ cokernel (α.app X))
    (CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
      (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α))
      (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
    (Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫ cokernel.π (α.app X))
have apply : Eq (α := Functor.obj (Functor.obj (evaluation C D) X) G ⟶ Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
  (CategoryStruct.comp (Y :=
    cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
    (CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
      (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α))
      (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
    (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
  (CategoryStruct.comp (Y :=
    cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
    (Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫ cokernel.π (α.app X))
    (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
Tactic: apply (cancel_mono (PreservesCokernel.iso ((evaluation C D).obj X) α).inv).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := Functor.obj (Functor.obj (evaluation C D) X) G ⟶ Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
    (CategoryStruct.comp (Y :=
      cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
      (CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
        (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α))
        (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
      (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
    (CategoryStruct.comp (Y :=
      cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
      (Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫ cokernel.π (α.app X))
      (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
have simp : Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α) ≫
    𝟙 (Functor.obj (Functor.obj (evaluation C D) X) (cokernel α)) =
  Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫
    CategoryStruct.comp (Y :=
      cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
      (cokernel.π (α.app X)) (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))
Tactic: simp only [Category.assoc, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α) ≫
      𝟙 (Functor.obj (Functor.obj (evaluation C D) X) (cokernel α)) =
    Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫
      CategoryStruct.comp (Y :=
        cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
        (cokernel.π (α.app X)) (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))
have dsimp : NatTrans.app (cokernel.π α) X ≫ 𝟙 ((cokernel α).obj X) =
  𝟙 (G.obj X) ≫
    CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
      (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ NatTrans.app (cokernel.π α) X ≫ 𝟙 ((cokernel α).obj X) =
    𝟙 (G.obj X) ≫
      CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
        (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))
have simp : Eq (α := G.obj X ⟶ (cokernel α).obj X) (NatTrans.app (cokernel.π α) X)
  (CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
    (cokernelComparison α (Functor.obj (evaluation C D) X)))
Tactic: simp only [PreservesCokernel.iso_inv, Category.id_comp, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := Abelian.coimage (α.app X) ⟶ Abelian.image (α.app X)) (coimageImageComparison (α.app X))
    (Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
      (coequalizer.π (kernel.ι (α.app X)) 0) (coimageImageComparison (α.app X)))
    (equalizer.ι (cokernel.π (α.app X)) 0) =
  CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
    (coequalizer.π (kernel.ι (α.app X)) 0 ≫
      Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
    (equalizer.ι (cokernel.π (α.app X)) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.FunctorCategory (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (coequalizer.π (kernel.ι (α.app X)) 0) (coimageImageComparison (α.app X)))
      (equalizer.ι (cokernel.π (α.app X)) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (coequalizer.π (kernel.ι (α.app X)) 0 ≫
        Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
      (equalizer.ι (cokernel.π (α.app X)) 0)
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
      (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
    (kernel.ι (cokernel.π (α.app X))) =
  CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
    (cokernel.π (kernel.ι (α.app X)) ≫
      Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
    (kernel.ι (cokernel.π (α.app X)))
Tactic: dsimp