mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
β : (projectiveResolution X).complex ⟶ P.complex
hβ : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β = P.iso.hom
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β) =
    (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β) ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
β : (projectiveResolution X).complex ⟶ P.complex
hβ : (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β = P.iso.hom
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app ((projectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β) =
    (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map β) ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
              (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
        HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
              (P.isoLeftDerivedToHomotopyCategoryObj G).inv
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙
              HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
              (P.isoLeftDerivedToHomotopyCategoryObj G).inv

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
            ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) ≫
        (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv =
    (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙
              HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
              ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
            (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map
              (P.isoLeftDerivedToHomotopyCategoryObj G).inv
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : ProjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Projective X
⊢ { X₁ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).X 1,
        X₂ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).X 0, X₃ := F.obj X,
        f := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).d 1 0,
        g := F.map (𝟙 X), zero := ⋯ }.Exact ∧
    Epi (F.map (𝟙 X))

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Projective X
⊢ { X₁ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).X 1,
        X₂ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).X 0, X₃ := F.obj X,
        f := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((ChainComplex.single₀ C).obj X)).d 1 0,
        g := F.map (𝟙 X), zero := ⋯ }.Exact ∧
    Epi (F.map (𝟙 X))
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as).homologyι 0 ≫
        HomologicalComplex.opcyclesMap
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
              (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)))
            0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F

Tactic:
← HomologicalComplex.homologyι_naturality_assoc

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      HomologicalComplex.homologyMap
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
            (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)))
          0 ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      HomologicalComplex.homologyMap
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
            (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)))
          0 ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj X).as) ≫
      HomologicalComplex.homologyMap
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
            (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y)))
          0 ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
          (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y))) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F

Tactic:
]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
X Y : C
f : X ⟶ Y
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map (F.leftDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((projectiveResolutions C).obj Y).as).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0).map
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map
          (ProjectiveResolution.lift f (projectiveResolution X) (projectiveResolution Y))) ≫
      (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex) ≫
        ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (projectiveResolution Y).complex).homologyι 0 ≫
          (projectiveResolution Y).fromLeftDerivedZero' F
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case pos
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : c.π c c (c.next i₁, i₂) = j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : ¬c.π c c (c.next i₁, i₂) = j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : ¬c.Rel i₁ (c.next i₁)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case pos
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i₁ i₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
h₂ : c.π c c (i₁, c.next i₂) = j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i₁ i₂ j : I
h₁ : c.Rel i₂ (c.next i₂)
h₂ : ¬c.π c c (i₁, c.next i₂) = j
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
i₁ i₂ j : I
h₁ : ¬c.Rel i₂ (c.next i₂)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Projective X
⊢ IsIso
    (((ProjectiveResolution.self X).isoLeftDerivedObj F 0).hom ≫
      (ChainComplex.isoHomologyι₀
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex)).hom ≫
        (ProjectiveResolution.self X).fromLeftDerivedZero' F)

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Projective X
⊢ IsIso
    (((ProjectiveResolution.self X).isoLeftDerivedObj F 0).hom ≫
      (ChainComplex.isoHomologyι₀
            ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj (ProjectiveResolution.self X).complex)).hom ≫
        (ProjectiveResolution.self X).fromLeftDerivedZero' F)
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ Nonempty
    (IsColimit
      (CokernelCofork.ofπ
        { X₁ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).X 1,
            X₂ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).X 0, X₃ := F.obj X,
            f := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).d 1 0, g := F.map (P.π.f 0),
            zero := ⋯ }.g
        ⋯))

Tactic:
]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteColimits F
X : C
P : ProjectiveResolution X
⊢ Nonempty
    (IsColimit
      (CokernelCofork.ofπ
        { X₁ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).X 1,
            X₂ := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).X 0, X₃ := F.obj X,
            f := ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).d 1 0, g := F.map (P.π.f 0),
            zero := ⋯ }.g
        ⋯))