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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n))
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K) ⟶
      Functor.obj (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
    (NatTrans.app (Iso.hom (homologyFunctorFactorsh C n))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
    (CategoryTheory.Functor.map (homologyFunctor C n) (NatTrans.app (Iso.hom (quotientCompQhIso C)) K) ≫
      NatTrans.app (Iso.hom (homologyFunctorFactors C n)) K ≫
        NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n)) K)

Tactic:
HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj ..

Premises used: HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj
-- 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
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n)
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K) ⟶
      Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n))
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
    (NatTrans.app (Iso.inv (homologyFunctorFactorsh C n))
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n)) K ≫
      NatTrans.app (Iso.inv (homologyFunctorFactors C n)) K ≫
        CategoryTheory.Functor.map (homologyFunctor C n) (NatTrans.app (Iso.inv (quotientCompQhIso C)) K))

Tactic:
HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj ..

Premises used: HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
mp :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f) →
    HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f
mpr :
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f →
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f) ↔
    HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f

Tactic:
constructor
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)
n : ℤ
mp :
  IsIso (X := Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) X)
    (CategoryTheory.Functor.map (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) f)
⊢ IsIso (X := Functor.obj (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n) X)
    (CategoryTheory.Functor.map (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n) f)

Tactic:
rw [← NatIso.isIso_map_iff (homologyFunctorFactorsh C n) f]

Premises used: DerivedCategory.homologyFunctorFactorsh, CategoryTheory.NatIso.isIso_map_iff
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)
n : ℤ
mp :
  IsIso (X := Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj Qh X))
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map Qh f))
⊢ IsIso (X := Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) X)
    (CategoryTheory.Functor.map (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) f)

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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)
n : ℤ
⊢ IsIso (X := Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj Qh X))
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map Qh f))

Tactic:
infer_instance
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f →
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)

Tactic:
Localization.inverts Qh (HomotopyCategory.quasiIso _ _) _

Premises used: DerivedCategory.Qh, HomotopyCategory.quasiIso, CategoryTheory.Localization.inverts
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f →
    IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)

Tactic:
exact Localization.inverts Qh (HomotopyCategory.quasiIso _ _) _

Premises used: DerivedCategory.Qh, HomotopyCategory.quasiIso, CategoryTheory.Localization.inverts
-- 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
n : ℤ
⊢ Functor.IsHomological (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n)

Tactic:
Functor.isHomological_of_localization Qh
    (homologyFunctor C n) _ (homologyFunctorFactorsh C n)

Premises used: DerivedCategory.Qh, DerivedCategory.homologyFunctor, CategoryTheory.Functor.isHomological_of_localization, DerivedCategory.homologyFunctorFactorsh
-- 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
n : ℤ
⊢ Eq (α := DerivedCategory.{w, v, u} C ⥤ C) (Functor.shift (homologyFunctor C 0) n) (homologyFunctor C n)

Tactic:
rfl

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.objPreimage, HomologicalComplexUpToQuasiIso.homologyFunctor, Classical.choose, CategoryTheory.Localization.lift, CategoryTheory.Functor.essImage.witness, CategoryTheory.Functor.shift, rfl
-- 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
K L : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
n : ℤ
f : K ⟶ Functor.obj (shiftFunctor (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)) n) L
a a' : ℤ
h : n + a = a'
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a) (Functor.obj Qh K) ⟶
      Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a') (Functor.obj Qh L))
    (Functor.shiftMap (homologyFunctor C 0) (ShiftedHom.map f Qh) a a' h)
    (NatTrans.app (Iso.hom (homologyFunctorFactorsh C a)) K ≫
      Functor.shiftMap (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' h ≫
        NatTrans.app (Iso.inv (homologyFunctorFactorsh C a')) L)

Tactic:
Functor.ShiftSequence.induced_shiftMap ..

Premises used: CategoryTheory.ShiftedHom.map, CategoryTheory.Functor.ShiftSequence.induced_shiftMap
-- 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
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
a a' : ℤ
h : n + a = a'
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a) (Functor.obj Q K) ⟶
      Functor.obj (C := DerivedCategory.{w, v, u} C) (Functor.shift (homologyFunctor C 0) a') (Functor.obj Q L))
    (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C 0) a)
        (NatTrans.app (Iso.inv (quotientCompQhIso C)) K) ≫
      ((CategoryTheory.Functor.map (homologyFunctor C a) (NatTrans.app (Iso.hom (quotientCompQhIso C)) K) ≫
            NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
              NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a)) K) ≫
          (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a)) K ≫
              Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' ⋯ ≫
                NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a')) L) ≫
            NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) a')) L ≫
              NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L ≫
                CategoryTheory.Functor.map (homologyFunctor C a') (NatTrans.app (Iso.inv (quotientCompQhIso C)) L)) ≫
        CategoryTheory.Functor.map (Functor.shift (homologyFunctor C 0) a')
          (NatTrans.app (Iso.hom (quotientCompQhIso C)) L))
    (NatTrans.app (Iso.hom (homologyFunctorFactors C a)) K ≫
      Functor.shiftMap (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0) f a a' h ≫
        NatTrans.app (Iso.inv (homologyFunctorFactors C a')) L)

Tactic:
simp [shift_homologyFunctor, ← Functor.map_comp, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, DerivedCategory.shift_homologyFunctor, CategoryTheory.Functor.map_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 (DerivedCategory.{w, v, u} C)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
rw : n₀ + 1 = n₁
rw₁ rw₂ : n₁ = n₁
⊢ 1 + n₀ = n₁

Tactic:
rw [add_comm 1, h]

Premises used: add_comm, OfNat.ofNat
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₂ ≫ δ T n₀ n₁ h = 0

Tactic:
(homologyFunctor C 0).comp_homologySequenceδ _ hT _ _ h

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.comp_homologySequenceδ, CategoryTheory.Functor.homologySequenceδ, OfNat.ofNat, DerivedCategory.HomologySequence.δ
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ δ T n₀ n₁ h ≫ CategoryTheory.Functor.map (homologyFunctor C n₁) T.mor₁ = 0

Tactic:
(homologyFunctor C 0).homologySequenceδ_comp _ hT _ _ h

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.homologySequenceδ, OfNat.ofNat, CategoryTheory.Functor.homologySequenceδ_comp, DerivedCategory.HomologySequence.δ
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ n₁ : ℤ
⊢ Eq (α := Functor.obj (homologyFunctor C n₀) T.obj₁ ⟶ Functor.obj (homologyFunctor C n₀) T.obj₃)
    (CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₁ ≫
      CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₂)
    0

Tactic:
simp only [← Functor.map_comp, comp_distTriang_mor_zero₁₂ _ hT,
        Functor.map_zero]

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ : ℤ
⊢ { X₁ := (homologyFunctor C n₀).obj T.obj₁, X₂ := (homologyFunctor C n₀).obj T.obj₂,
      X₃ := (homologyFunctor C n₀).obj T.obj₃, f := CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₁,
      g := CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₂, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
(homologyFunctor C 0).homologySequence_exact₂ _ hT _

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.homologySequence_exact₂, OfNat.ofNat
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (homologyFunctor C n₀).obj T.obj₂, X₂ := (homologyFunctor C n₀).obj T.obj₃,
      X₃ := (homologyFunctor C n₁).obj T.obj₁, f := CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₂,
      g := δ T n₀ n₁ h, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
(homologyFunctor C 0).homologySequence_exact₃ _ hT _ _ h

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.Functor.homologySequenceδ, OfNat.ofNat, DerivedCategory.HomologySequence.δ
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := (homologyFunctor C n₀).obj T.obj₃, X₂ := (homologyFunctor C n₁).obj T.obj₁,
      X₃ := (homologyFunctor C n₁).obj T.obj₂, f := δ T n₀ n₁ h,
      g := CategoryTheory.Functor.map (homologyFunctor C n₁) T.mor₁, zero := ⋯ : ShortComplex.{v, u} C }.Exact

Tactic:
(homologyFunctor C 0).homologySequence_exact₁ _ hT _ _ h

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.homologySequenceδ, CategoryTheory.Functor.homologySequence_exact₁, OfNat.ofNat, DerivedCategory.HomologySequence.δ
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ : ℤ
⊢ Epi (X := Functor.obj (homologyFunctor C n₀) T.obj₁) (CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₁) ↔
    Eq (α := Functor.obj (homologyFunctor C n₀) T.obj₂ ⟶ Functor.obj (homologyFunctor C n₀) T.obj₃)
      (CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₂) 0

Tactic:
(homologyFunctor C 0).homologySequence_epi_shift_map_mor₁_iff _ hT _

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, OfNat.ofNat
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Mono (X := Functor.obj (homologyFunctor C n₁) T.obj₁) (CategoryTheory.Functor.map (homologyFunctor C n₁) T.mor₁) ↔
    δ T n₀ n₁ h = 0

Tactic:
(homologyFunctor C 0).homologySequence_mono_shift_map_mor₁_iff _ hT _ _ h

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, CategoryTheory.Functor.homologySequenceδ, OfNat.ofNat, DerivedCategory.HomologySequence.δ
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Epi (X := Functor.obj (homologyFunctor C n₀) T.obj₂) (CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₂) ↔
    δ T n₀ n₁ h = 0

Tactic:
(homologyFunctor C 0).homologySequence_epi_shift_map_mor₂_iff _ hT _ _ h

Premises used: DerivedCategory.homologyFunctor, CategoryTheory.Functor.homologySequenceδ, OfNat.ofNat, DerivedCategory.HomologySequence.δ, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff
-- 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 (DerivedCategory.{w, v, u} C)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ instPreadditive ⋯ _) T
n₀ : ℤ
⊢ Mono (X := Functor.obj (homologyFunctor C n₀) T.obj₂) (CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₂) ↔
    Eq (α := Functor.obj (homologyFunctor C n₀) T.obj₁ ⟶ Functor.obj (homologyFunctor C n₀) T.obj₂)
      (CategoryTheory.Functor.map (homologyFunctor C n₀) T.mor₁) 0

Tactic:
(homologyFunctor C 0).homologySequence_mono_shift_map_mor₂_iff _ hT n₀

Premises used: DerivedCategory.homologyFunctor, OfNat.ofNat, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff
-- 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 ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁

Tactic:
lia
-- 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 ℤ)
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₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₁))
      (Functor.shiftMap (DerivedCategory.homologyFunctor C 0)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁)
        n₀ n₁ ⋯)
      (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁))
⊢ Eq (α :=
    Functor.obj
        (Functor.comp (D := DerivedCategory.{w, v, u} C) DerivedCategory.Q (DerivedCategory.homologyFunctor C n₀))
        T.obj₃ ⟶
      homology T.obj₁ n₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
    (DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h ≫
      NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁)

Tactic:
dsimp [DerivedCategory.HomologySequence.δ]

Premises used: DerivedCategory.HomologySequence.δ
-- 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 ℤ)
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₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₁))
      (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫
        Functor.shiftMap (homologyFunctor C (ComplexShape.up ℤ) 0) T.mor₃ n₀ n₁ ⋯ ≫
          NatTrans.app (Iso.inv (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁)
      (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁))
⊢ Eq (α :=
    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₃ ≫ homologyδOfTriangle T n₀ n₁ h)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₁))
      (Functor.shiftMap (DerivedCategory.homologyFunctor C 0)
        (CategoryTheory.Functor.map DerivedCategory.Q T.mor₃ ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q 1)) T.obj₁)
        n₀ n₁ ⋯)
      (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁))

Tactic:
rw [dsimp% [ShiftedHom.map]
      DerivedCategory.shiftMap_homologyFunctor_map_Q T.mor₃ n₀ n₁ (by lia)]

Premises used: CategoryTheory.ShiftedHom.map, DerivedCategory.shiftMap_homologyFunctor_map_Q, CategoryTheory.Pretriangulated.Triangle.mor₃
-- 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 ℤ)
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₁)
    (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (DerivedCategory.homologyFunctor C n₁)
        (Functor.obj DerivedCategory.Q T.obj₁))
      (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₀)) T.obj₃ ≫
        Functor.shiftMap (homologyFunctor C (ComplexShape.up ℤ) 0) T.mor₃ n₀ n₁ ⋯ ≫
          NatTrans.app (Iso.inv (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁)
      (NatTrans.app (Iso.hom (DerivedCategory.homologyFunctorFactors C n₁)) T.obj₁))

Tactic:
simp [Functor.shiftMap, homologyFunctor_shift, homologyδOfTriangle]

Premises used: CochainComplex.homologyδOfTriangle, CochainComplex.homologyFunctor_shift, CategoryTheory.Functor.shiftMap