awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
w :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj Qh (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
      𝟙
        (Functor.obj HomologicalComplexUpToQuasiIso.Q
          (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
        𝟙 (Functor.obj (singleFunctor C n) X) ≫
          𝟙
            (Functor.obj HomologicalComplexUpToQuasiIso.Q
              (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X) :
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))

Tactic:
rw [CategoryTheory.Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
w :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙
      (Functor.obj HomologicalComplexUpToQuasiIso.Q
        (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj Qh (Functor.obj (SingleFunctors.functor (HomotopyCategory.singleFunctors C) n) X)) ≫
      𝟙
        (Functor.obj HomologicalComplexUpToQuasiIso.Q
          (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))

Tactic:
erw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙
      (Functor.obj HomologicalComplexUpToQuasiIso.Q
        (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
    (𝟙 (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
w :
  ∀ (X : C),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C)
        (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
      (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) n) X)
      (NatTrans.app (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n)) X)
⊢ Eq (α :=
    Quiver.Hom (V := C ⥤ DerivedCategory.{w, v, u} C)
      (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n)
      (SingleFunctors.functor (singleFunctors C) n))
    (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) n)
    (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n))

Tactic:
ext X
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
w :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X))
      (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
    (NatTrans.app (Iso.inv (quotientCompQhIso C))
      (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X))
    (𝟙 (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Functor.obj (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) n) X)
    (NatTrans.app (𝟙 (SingleFunctors.functor (SingleFunctors.postcomp (CochainComplex.singleFunctors C) Q) n)) X)

Tactic:
simp [singleFunctorsPostcompQIso, HomotopyCategory.singleFunctorsPostcompQuotientIso]

Premises used: DerivedCategory.singleFunctorsPostcompQIso, HomotopyCategory.singleFunctorsPostcompQuotientIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X : C
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C)
      (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X))
      (Functor.obj (SingleFunctors.functor (singleFunctors C) n) X))
    (NatTrans.app (Iso.inv (quotientCompQhIso C))
      (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X))
    (𝟙 (Functor.obj Q (Functor.obj (SingleFunctors.functor (CochainComplex.singleFunctors C) n) X)))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
φ : K ⟶ L
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q K) (CategoryTheory.Functor.map Q φ) ↔ QuasiIso φ

Tactic:
apply HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso

Premises used: HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
f g : K ⟶ L
h : Homotopy f g
⊢ Eq.{w + 1} (α := Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K) (Functor.obj Q L))
    (CategoryTheory.Functor.map Q f) (CategoryTheory.Functor.map Q g)

Tactic:
HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy h

Premises used: HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
X Y : CochainComplex.{v₁, u₁, 0} C₁ ℤ
f : X ⟶ Y
⊢ Eq.{w₂ + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
      (obj (C := DerivedCategory.{w₁, v₁, u₁} C₁) F.mapDerivedCategory (obj DerivedCategory.Q X))
      (obj (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q) Y))
    (map F.mapDerivedCategory (map DerivedCategory.Q f) ≫ NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) Y)
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) X ≫
      map DerivedCategory.Q (map (F.mapHomologicalComplex (ComplexShape.up ℤ)) f))

Tactic:
F.mapDerivedCategoryFactors.hom.naturality f

Premises used: CategoryTheory.Functor.mapDerivedCategoryFactors, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
K : CochainComplex.{v₁, u₁, 0} C₁ ℤ
⊢ Eq.{w₂ + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
      (obj (comp (D := DerivedCategory.{w₁, v₁, u₁} C₁) DerivedCategory.Qh F.mapDerivedCategory)
        (obj (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) K))
      (obj (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
        (obj (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) K)))
    (NatTrans.app (Iso.hom F.mapDerivedCategoryFactorsh) (obj (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) K))
    (map F.mapDerivedCategory (NatTrans.app (Iso.hom (DerivedCategory.quotientCompQhIso C₁)) K) ≫
      NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) K ≫
        NatTrans.app (Iso.inv (DerivedCategory.quotientCompQhIso C₂))
            (obj (F.mapHomologicalComplex (ComplexShape.up ℤ)) K) ≫
          map DerivedCategory.Qh (NatTrans.app (Iso.inv (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) K))

Tactic:
F.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app K

Premises used: CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
⊢ NatTrans.CommShift (C := HomotopyCategory.{v₁, u₁, 0} C₁ (ComplexShape.up ℤ)) (D := DerivedCategory.{w₂, v₂, u₂} C₂)
    (F₁ := comp (D := DerivedCategory.{w₁, v₁, u₁} C₁) DerivedCategory.Qh F.mapDerivedCategory)
    (Iso.hom F.mapDerivedCategoryFactorsh) ℤ

Tactic:
inferInstanceAs (NatTrans.CommShift (Localization.Lifting.iso
      DerivedCategory.Qh (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ))
        (F.mapHomotopyCategory _ ⋙ DerivedCategory.Qh)
          F.mapDerivedCategory).hom ℤ)

Premises used: _private.0.CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh._proof_1
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
w :
  ∀ (K : CochainComplex.{v₁, u₁, 0} C₁ ℤ),
    Eq.{w₂ + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
        (obj (comp (D := DerivedCategory.{w₁, v₁, u₁} C₁) DerivedCategory.Q F.mapDerivedCategory) K)
        (obj (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q) K))
      (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors) K)
      (NatTrans.app
        (whiskerRight (Iso.inv (DerivedCategory.quotientCompQhIso C₁)) F.mapDerivedCategory ≫
          Iso.hom
              (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) DerivedCategory.Qh F.mapDerivedCategory) ≫
            whiskerLeft (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) (Iso.hom F.mapDerivedCategoryFactorsh) ≫
              Iso.inv
                  (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ))
                    (F.mapHomotopyCategory (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
                whiskerRight (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) DerivedCategory.Qh ≫
                  Iso.hom
                      (associator (F.mapHomologicalComplex (ComplexShape.up ℤ))
                        (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
                    whiskerLeft (F.mapHomologicalComplex (ComplexShape.up ℤ))
                      (Iso.hom (DerivedCategory.quotientCompQhIso C₂)))
        K)
⊢ Eq (α :=
    Quiver.Hom (V := CochainComplex.{v₁, u₁, 0} C₁ ℤ ⥤ DerivedCategory.{w₂, v₂, u₂} C₂)
      (comp (D := DerivedCategory.{w₁, v₁, u₁} C₁) DerivedCategory.Q F.mapDerivedCategory)
      (F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q))
    (Iso.hom F.mapDerivedCategoryFactors)
    (whiskerRight (Iso.inv (DerivedCategory.quotientCompQhIso C₁)) F.mapDerivedCategory ≫
      Iso.hom (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) DerivedCategory.Qh F.mapDerivedCategory) ≫
        whiskerLeft (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) (Iso.hom F.mapDerivedCategoryFactorsh) ≫
          Iso.inv
              (associator (HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)) (F.mapHomotopyCategory (ComplexShape.up ℤ))
                DerivedCategory.Qh) ≫
            whiskerRight (Iso.hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ))) DerivedCategory.Qh ≫
              Iso.hom
                  (associator (F.mapHomologicalComplex (ComplexShape.up ℤ))
                    (HomotopyCategory.quotient C₂ (ComplexShape.up ℤ)) DerivedCategory.Qh) ≫
                whiskerLeft (F.mapHomologicalComplex (ComplexShape.up ℤ))
                  (Iso.hom (DerivedCategory.quotientCompQhIso C₂)))

Tactic:
ext K
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
⊢ IsTriangulated (C := DerivedCategory.{w₁, v₁, u₁} C₁) (D := DerivedCategory.{w₂, v₂, u₂} C₂) F.mapDerivedCategory

Tactic:
Functor.isTriangulated_of_precomp_iso F.mapDerivedCategoryFactorsh

Premises used: CategoryTheory.Functor.isTriangulated_of_precomp_iso, CategoryTheory.Functor.mapDerivedCategoryFactorsh
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v₁, u₁} R C₁
inst_11 : CategoryTheory.Linear.{u_1, v₂, u₂} R C₂
inst_12 : Linear R F
rw :
  Linear R (C := HomotopyCategory.{v₁, u₁, 0} C₁ (ComplexShape.up ℤ)) (D := DerivedCategory.{w₂, v₂, u₂} C₂)
    (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)
⊢ Linear R (C := DerivedCategory.{w₁, v₁, u₁} C₁) (D := DerivedCategory.{w₂, v₂, u₂} C₂) F.mapDerivedCategory

Tactic:
rw [← Localization.functor_linear_iff DerivedCategory.Qh (HomotopyCategory.quasiIso C₁
    (ComplexShape.up ℤ)) R ((F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh)]

Premises used: CategoryTheory.Localization.functor_linear_iff, DerivedCategory.Qh, CategoryTheory.Functor.comp, Int, HomotopyCategory.quasiIso, CategoryTheory.Functor.mapHomotopyCategory, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
R : Type u_1
inst_9 : Ring R
inst_10 : CategoryTheory.Linear.{u_1, v₁, u₁} R C₁
inst_11 : CategoryTheory.Linear.{u_1, v₂, u₂} R C₂
inst_12 : Linear R F
⊢ Linear R (C := HomotopyCategory.{v₁, u₁, 0} C₁ (ComplexShape.up ℤ)) (D := DerivedCategory.{w₂, v₂, u₂} C₂)
    (F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
X : C₁
⊢ Eq.{w₂ + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
      (obj DerivedCategory.Q
        (obj (C := CochainComplex.{v₁, u₁, 0} C₁ ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
          (obj (HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0) X)))
      (obj (DerivedCategory.singleFunctor C₂ 0) (F.obj X)))
    (CategoryStruct.comp (Y :=
        obj (C := DerivedCategory.{w₁, v₁, u₁} C₁) F.mapDerivedCategory (obj (DerivedCategory.singleFunctor C₁ 0) X))
        (NatTrans.app (Iso.inv F.mapDerivedCategoryFactors)
          (obj (HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0) X))
        (NatTrans.app (Iso.hom (F.mapDerivedCategorySingleFunctor 0)) X) :
      Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
        (obj DerivedCategory.Q
          (obj (C := CochainComplex.{v₁, u₁, 0} C₁ ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (obj (HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0) X)))
        (obj (DerivedCategory.singleFunctor C₂ 0) (F.obj X)))
    (map DerivedCategory.Q (NatTrans.app (Iso.hom (F.mapCochainComplexSingleFunctor 0)) X) :
      Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
        (obj DerivedCategory.Q
          (obj (C := CochainComplex.{v₁, u₁, 0} C₁ ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (obj (CochainComplex.singleFunctor C₁ 0) X)))
        (obj DerivedCategory.Q (obj (CochainComplex.singleFunctor C₂ 0) (F.obj X))))

Tactic:
simp [Functor.mapDerivedCategorySingleFunctor, Functor.mapCochainComplexSingleFunctor,
    CochainComplex.singleFunctor, CochainComplex.singleFunctors,
    DerivedCategory.singleFunctorIsoCompQ]

Premises used: CochainComplex.singleFunctor, DerivedCategory.singleFunctorIsoCompQ, CategoryTheory.Functor.mapCochainComplexSingleFunctor, CochainComplex.singleFunctors, CategoryTheory.Functor.mapDerivedCategorySingleFunctor
-- Module: Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
inst_1 : Abelian.{v₁, u₁} C₁
inst_2 : HasDerivedCategory.{w₁, v₁, u₁} C₁
C₂ : Type u₂
inst_3 : Category.{v₂, u₂} C₂
inst_4 : Abelian.{v₂, u₂} C₂
inst_5 : HasDerivedCategory.{w₂, v₂, u₂} C₂
F : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
inst_6 : F.Additive
inst_7 : PreservesFiniteLimits F
inst_8 : PreservesFiniteColimits F
X : C₁
⊢ Eq.{w₂ + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂) (obj (DerivedCategory.singleFunctor C₂ 0) (F.obj X))
      (obj DerivedCategory.Q
        (obj (C := CochainComplex.{v₁, u₁, 0} C₁ ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
          (obj (HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0) X))))
    (CategoryStruct.comp (Y :=
        obj (C := DerivedCategory.{w₁, v₁, u₁} C₁) F.mapDerivedCategory (obj (DerivedCategory.singleFunctor C₁ 0) X))
        (NatTrans.app (Iso.inv (F.mapDerivedCategorySingleFunctor 0)) X)
        (NatTrans.app (Iso.hom F.mapDerivedCategoryFactors)
          (obj (HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0) X)) :
      Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂) (obj (DerivedCategory.singleFunctor C₂ 0) (F.obj X))
        (obj DerivedCategory.Q
          (obj (C := CochainComplex.{v₁, u₁, 0} C₁ ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (obj (HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0) X))))
    (map DerivedCategory.Q (NatTrans.app (Iso.inv (F.mapCochainComplexSingleFunctor 0)) X) :
      Quiver.Hom (V := DerivedCategory.{w₂, v₂, u₂} C₂)
        (obj DerivedCategory.Q (obj (CochainComplex.singleFunctor C₂ 0) (F.obj X)))
        (obj DerivedCategory.Q
          (obj (C := CochainComplex.{v₁, u₁, 0} C₁ ℤ) (F.mapHomologicalComplex (ComplexShape.up ℤ))
            (obj (CochainComplex.singleFunctor C₁ 0) X))))

Tactic:
simp [Functor.mapDerivedCategorySingleFunctor, Functor.mapCochainComplexSingleFunctor,
    CochainComplex.singleFunctor, CochainComplex.singleFunctors,
    DerivedCategory.singleFunctorIsoCompQ]

Premises used: CochainComplex.singleFunctor, DerivedCategory.singleFunctorIsoCompQ, CategoryTheory.Functor.mapCochainComplexSingleFunctor, CochainComplex.singleFunctors, CategoryTheory.Functor.mapDerivedCategorySingleFunctor
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
⊢ (ComplexShape.up ℤ).prev i = i - 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
⊢ i - 1 < i

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
rw : ι.f i ≫ e.hom = (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α) ≫ e.hom
⊢ ι.f i = Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α

Tactic:
rw [← cancel_mono e.hom]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
I : C
inst_2 : Injective.{v, u} I
L : CochainComplex.{v, u, 0} C ℤ
i : ℤ
ι : Functor.obj (singleFunctor C i) I ⟶ L
inst_3 : L.IsStrictlyGE i
inst_4 : QuasiIsoAt ι i
e : L.X i ≅ opcycles L i := pOpcyclesIso L (i - 1) i ⋯ ⋯
α : I ⟶ L.X i := Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫ homologyMap ι i ≫ homologyι L i ≫ e.inv
dsimp :
  Eq (α := X.{v, u, 0} (Functor.obj (singleFunctor C i) I) i ⟶ opcycles L i) (ι.f i ≫ pOpcycles L i)
    ((Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫
        Iso.inv (singleObjHomologySelfIso (ComplexShape.up ℤ) i I) ≫
          CategoryStruct.comp (Y := homology L i) (homologyMap ι i)
            (homologyι L i ≫ Iso.inv (pOpcyclesIso L (i - 1) i ⋯ ⋯))) ≫
      pOpcycles L i)
⊢ ι.f i ≫ e.hom = (Iso.hom (singleObjXSelf (ComplexShape.up ℤ) i I) ≫ α) ≫ e.hom

Tactic:
dsimp [α, e]