awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw :
  Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
        T.obj₃ ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
          (Triangle.obj₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)))
        (DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ ⋯)
        (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
          NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
      Functor.obj
          (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
          T.obj₃ ⟶
        homology T.obj₂ n₁)
⊢ Eq (α := homology T.obj₃ n₀ ⟶ homology T.obj₂ n₁) (homologyδOfTriangle T n₀ n₁ h ≫ homologyMap T.mor₁ n₁) 0

Tactic:
rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc ..,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality]

Premises used: DerivedCategory.homologyFunctorFactors_hom_naturality, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, DerivedCategory.homologyFunctorFactors, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
dsimp :
  Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
          (Functor.obj DerivedCategory.Q T.obj₁))
        (DerivedCategory.HomologySequence.δ
          (Triangle.mk (X := Functor.obj DerivedCategory.Q T.obj₁) (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₂)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁))
          n₀ n₁ ⋯)
        (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
          NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
⊢ Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
        T.obj₃ ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
          (Triangle.obj₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)))
        (DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ ⋯)
        (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
          NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
      Functor.obj
          (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
          T.obj₃ ⟶
        homology T.obj₂ n₁)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw :
  Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₂))
      0 (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0)
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
        Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
          (Functor.obj DerivedCategory.Q T.obj₁))
        (DerivedCategory.HomologySequence.δ
          (Triangle.mk (X := Functor.obj DerivedCategory.Q T.obj₁) (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₂)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁))
          n₀ n₁ ⋯)
        (CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
            (CategoryTheory.Functor.map DerivedCategory.Q T.mor₁) ≫
          NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂) :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0 :
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
          (Functor.obj DerivedCategory.Q T.obj₃) ⟶
        homology T.obj₂ n₁)

Tactic:
rw [reassoc_of% dsimp% DerivedCategory.HomologySequence.δ_comp _ hT n₀ n₁ h]

Premises used: DerivedCategory.HomologySequence.δ_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₀)
        (Functor.obj DerivedCategory.Q T.obj₃) ⟶
      homology T.obj₂ n₁)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₂))
      0 (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₂))
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Eq (α := homology T.obj₂ n₀ ⟶ homology T.obj₁ n₁) (homologyMap T.mor₂ n₀ ≫ homologyδOfTriangle T n₀ n₁ h) 0

Tactic:
simp [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    ← DerivedCategory.homologyFunctorFactors_hom_naturality_assoc,
    reassoc_of% dsimp% DerivedCategory.HomologySequence.comp_δ _ hT n₀ n₁ h]

Premises used: DerivedCategory.HomologySequence.comp_δ, DerivedCategory.homologyFunctorFactors, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, DerivedCategory.homologyFunctorFactors_hom_naturality_assoc
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := homology T.obj₃ n₀, X₂ := homology T.obj₁ n₁, X₃ := homology T.obj₂ n₁, f := homologyδOfTriangle T n₀ n₁ h,
      g := homologyMap T.mor₁ n₁, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₁ _ hT n₀ n₁ h)

Premises used: CategoryTheory.ShortComplex.exact_of_iso, DerivedCategory.HomologySequence.exact₁
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
refine :
  { X₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      X₂ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      f := DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h,
      g :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
          (Triangle.mor₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      zero := ⋯ : ShortComplex.{v, u} C } ≅
    { X₁ := homology T.obj₃ n₀, X₂ := homology T.obj₁ n₁, X₃ := homology T.obj₂ n₁, f := homologyδOfTriangle T n₀ n₁ h,
      g := homologyMap T.mor₁ n₁, zero := ⋯ }
⊢ { X₁ := homology T.obj₃ n₀, X₂ := homology T.obj₁ n₁, X₃ := homology T.obj₂ n₁, f := homologyδOfTriangle T n₀ n₁ h,
      g := homologyMap T.mor₁ n₁, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₁ _ hT n₀ n₁ h)

Premises used: CategoryTheory.ShortComplex.exact_of_iso, DerivedCategory.HomologySequence.exact₁
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      X₂ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      f := DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h,
      g :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
          (Triangle.mor₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      zero := ⋯ : ShortComplex.{v, u} C } ≅
    { X₁ := homology T.obj₃ n₀, X₂ := homology T.obj₁ n₁, X₃ := homology T.obj₂ n₁, f := homologyδOfTriangle T n₀ n₁ h,
      g := homologyMap T.mor₁ n₁, zero := ⋯ }

Tactic:
exact ShortComplex.isoMk
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)

Premises used: CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
⊢ { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₂ _ hT n)

Premises used: DerivedCategory.HomologySequence.exact₂, CategoryTheory.ShortComplex.exact_of_iso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
refine :
  { X₁ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      X₂ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      X₃ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      f :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
          (Triangle.mor₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      g :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
          (Triangle.mor₂ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      zero := ⋯ : ShortComplex.{v, u} C } ≅
    { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ }
⊢ { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₂ _ hT n)

Premises used: DerivedCategory.HomologySequence.exact₂, CategoryTheory.ShortComplex.exact_of_iso
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
⊢ { X₁ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      X₂ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      X₃ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      f :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
          (Triangle.mor₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      g :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
          (Triangle.mor₂ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      zero := ⋯ : ShortComplex.{v, u} C } ≅
    { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ }

Tactic:
exact ShortComplex.isoMk
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)

Premises used: CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₃ _ hT n₀ n₁ h)

Premises used: CategoryTheory.ShortComplex.exact_of_iso, DerivedCategory.HomologySequence.exact₃
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
refine :
  { X₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      X₂ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      f :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₀)
          (Triangle.mor₂ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      g := DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h,
      zero := ⋯ : ShortComplex.{v, u} C } ≅
    { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ }
⊢ { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₃ _ hT n₀ n₁ h)

Premises used: CategoryTheory.ShortComplex.exact_of_iso, DerivedCategory.HomologySequence.exact₃
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      X₂ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      f :=
        CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₀)
          (Triangle.mor₂ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
      g := DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h,
      zero := ⋯ : ShortComplex.{v, u} C } ≅
    { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ }

Tactic:
exact ShortComplex.isoMk
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)

Premises used: CategoryTheory.ShortComplex.isoMk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{u_1, v, u} C
K : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
L : CochainComplex.{v, u, 0} C ℤ
inst_3 : L.IsKInjective
⊢ Function.Bijective.{v + 1, u_1 + 1} (α := K ⟶ Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L) (β :=
    Quiver.Hom (V := DerivedCategory.{u_1, v, u} C) (Functor.obj Qh K)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
    (CategoryTheory.Functor.map Qh)

Tactic:
(CochainComplex.IsKInjective.rightOrthogonal L).map_bijective_of_isTriangulated _ _

Premises used: CochainComplex.IsKInjective.rightOrthogonal, CategoryTheory.ObjectProperty.rightOrthogonal.map_bijective_of_isTriangulated
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩

Premises used: homotopyEquivalences_le_quasiIso, Int, Iff.intro, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
refine : QuasiIso f → homotopyEquivalences C (ComplexShape.up ℤ) f
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
h : QuasiIso f
rw :
  IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
⊢ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.MorphismProperty.inverseImage_iff, HomotopyCategory.inverseImage_quotient_isomorphisms