awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
a : ℤ
K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)
w :
  Eq (α :=
    (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0) K).homology a ⟶
      K.homology a)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C 0 a a ⋯)) K :
      Functor.obj
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙
            homologyFunctor C (up ℤ) a)
          K ⟶
        Functor.obj (homologyFunctor C (up ℤ) a) K)
    (ShortComplex.homologyMap
        (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)) K)) ≫
      𝟙 (K.homology a))
⊢ Eq (α :=
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙
          homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a) K)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C 0 a a ⋯)) K)
    (NatTrans.app
      (Iso.hom
        (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)
            (homologyFunctor C (up ℤ) a) ≪≫
          Functor.leftUnitor (homologyFunctor C (up ℤ) a)))
      K)

Tactic:
dsimp [homologyMap]

Premises used: HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
a : ℤ
K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)
⊢ Eq (α :=
    (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0) K).homology a ⟶
      K.homology a)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C 0 a a ⋯)) K :
      Functor.obj
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (A := ℤ) 0 ⋙
            homologyFunctor C (up ℤ) a)
          K ⟶
        Functor.obj (homologyFunctor C (up ℤ) a) K)
    (ShortComplex.homologyMap
        (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (shiftFunctorZero (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) ℤ)) K)) ≫
      𝟙 (K.homology a))

Tactic:
simp only [ShiftSequence.shiftIso_hom_app, comp_id,
      shiftShortComplexFunctorIso_zero_add_hom_app]

Premises used: CategoryTheory.Category.comp_id, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, CochainComplex.ShiftSequence.shiftIso_hom_app
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
w :
  ∀ (K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)),
    Eq (α :=
      Functor.obj
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
          K ⟶
        Functor.obj (homologyFunctor C (up ℤ) a'') K)
      (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C (m + n) a a'' ⋯)) K)
      (NatTrans.app
        (Iso.hom
          (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)
              (homologyFunctor C (up ℤ) a) ≪≫
            Functor.associator (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n)
                (homologyFunctor C (up ℤ) a) ≪≫
              Functor.isoWhiskerLeft (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
                  (ShiftSequence.shiftIso C n a a' ha') ≪≫
                ShiftSequence.shiftIso C m a' a'' ha''))
        K)
⊢ Eq (α :=
    Iso (C := HomologicalComplex.{v_1, u_1, 0} C (up ℤ) ⥤ C)
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
      (homologyFunctor C (up ℤ) a''))
    (ShiftSequence.shiftIso C (m + n) a a'' ⋯)
    (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)
        (homologyFunctor C (up ℤ) a) ≪≫
      Functor.associator (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) (homologyFunctor C (up ℤ) a) ≪≫
        Functor.isoWhiskerLeft (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
            (ShiftSequence.shiftIso C n a a' ha') ≪≫
          ShiftSequence.shiftIso C m a' a'' ha'')

Tactic:
ext K
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)
w :
  Eq (α :=
    (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n)) K).homology a ⟶
      K.homology a'')
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C (m + n) a a'' ⋯)) K :
      Functor.obj
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
          K ⟶
        Functor.obj (homologyFunctor C (up ℤ) a'') K)
    (ShortComplex.homologyMap
        (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)) K)) ≫
      𝟙
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n)
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K)).homology
            a) ≫
        CategoryStruct.comp (Y :=
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K).homology a')
          (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C n a a' ha'))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K) :
            Functor.obj
                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n ⋙ homologyFunctor C (up ℤ) a)
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K) ⟶
              Functor.obj (homologyFunctor C (up ℤ) a')
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K))
          (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C m a' a'' ha'')) K))
⊢ Eq (α :=
    Functor.obj
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
        K ⟶
      Functor.obj (homologyFunctor C (up ℤ) a'') K)
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C (m + n) a a'' ⋯)) K)
    (NatTrans.app
      (Iso.hom
        (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)
            (homologyFunctor C (up ℤ) a) ≪≫
          Functor.associator (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
              (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n)
              (homologyFunctor C (up ℤ) a) ≪≫
            Functor.isoWhiskerLeft (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m)
                (ShiftSequence.shiftIso C n a a' ha') ≪≫
              ShiftSequence.shiftIso C m a' a'' ha''))
      K)

Tactic:
dsimp [homologyMap]

Premises used: HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)
⊢ Eq (α :=
    (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n)) K).homology a ⟶
      K.homology a'')
    (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C (m + n) a a'' ⋯)) K :
      Functor.obj
          (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) (m + n) ⋙ homologyFunctor C (up ℤ) a)
          K ⟶
        Functor.obj (homologyFunctor C (up ℤ) a'') K)
    (ShortComplex.homologyMap
        (CategoryTheory.Functor.map (shortComplexFunctor C (up ℤ) a)
          (NatTrans.app (Iso.hom (shiftFunctorAdd (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m n)) K)) ≫
      𝟙
          ((Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n)
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K)).homology
            a) ≫
        CategoryStruct.comp (Y :=
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K).homology a')
          (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C n a a' ha'))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K) :
            Functor.obj
                (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n ⋙ homologyFunctor C (up ℤ) a)
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K) ⟶
              Functor.obj (homologyFunctor C (up ℤ) a')
                (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) m) K))
          (NatTrans.app (Iso.hom (ShiftSequence.shiftIso C m a' a'' ha'')) K))

Tactic:
simp only [ShiftSequence.shiftIso_hom_app, id_comp,
      ← ShortComplex.homologyMap_comp, shiftFunctorAdd'_eq_shiftFunctorAdd,
      shiftShortComplexFunctorIso_add'_hom_app n m _ rfl a a' a'' ha' ha'' K]

Premises used: CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, CategoryTheory.ShortComplex.homologyMap_comp, rfl, CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, CategoryTheory.Category.id_comp, CochainComplex.ShiftSequence.shiftIso_hom_app
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
simp :
  IsIso (X := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K).homology i)
      (Y := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) L).homology i)
      (homologyMap
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) i) ↔
    IsIso (X := homology K j) (Y := homology L j) (homologyMap φ j)
⊢ QuasiIsoAt (K := Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K)
      (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) i ↔
    QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]

Premises used: quasiIsoAt_iff_isIso_homologyMap
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ IsIso (X := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K).homology i)
      (Y := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) L).homology i)
      (homologyMap
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) i) ↔
    IsIso (X := homology K j) (Y := homology L j) (homologyMap φ j)

Tactic:
(NatIso.isIso_map_iff
    ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i j h) φ)

Premises used: HomologicalComplex.homologyFunctor, CategoryTheory.ShortComplex.leftHomologyMap', Int, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.Functor.shiftIso, CategoryTheory.NatIso.isIso_map_iff, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, OfNat.ofNat, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ IsIso (X := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K).homology i)
      (Y := (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) L).homology i)
      (homologyMap
        (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) i) ↔
    IsIso (X := homology K j) (Y := homology L j) (homologyMap φ j)

Tactic:
exact (NatIso.isIso_map_iff
    ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i j h) φ)

Premises used: HomologicalComplex.homologyFunctor, Int, CategoryTheory.Functor.shiftIso, CategoryTheory.NatIso.isIso_map_iff, OfNat.ofNat, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
simp : (∀ (i : ℤ), QuasiIsoAt φ (n + i)) ↔ ∀ (i : ℤ), QuasiIsoAt φ i
⊢ QuasiIso (K := Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K)
      (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ) ↔
    QuasiIso φ

Tactic:
simp only [quasiIso_iff, fun i ↦ quasiIsoAt_shift_iff φ n i _ rfl]

Premises used: CochainComplex.quasiIsoAt_shift_iff, quasiIso_iff, HAdd.hAdd, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
mp : (∀ (i : ℤ), QuasiIsoAt φ (n + i)) → ∀ (i : ℤ), QuasiIsoAt φ i
mpr : (∀ (i : ℤ), QuasiIsoAt φ i) → ∀ (i : ℤ), QuasiIsoAt φ (n + i)
⊢ (∀ (i : ℤ), QuasiIsoAt φ (n + i)) ↔ ∀ (i : ℤ), QuasiIsoAt φ i

Tactic:
constructor
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ (n + i)
j : ℤ
⊢ j = n + (j - n)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ (n + i)
j : ℤ
mp : ∀ (i : ℤ), QuasiIsoAt φ (n + i)
⊢ QuasiIsoAt φ j

Tactic:
obtain ⟨i, rfl⟩ : ∃ i, j = n + i := ⟨j - n, by lia⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ (n + i)
i : ℤ
⊢ QuasiIsoAt φ (n + i)

Tactic:
h i
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ (n + i)
i : ℤ
⊢ QuasiIsoAt φ (n + i)

Tactic:
exact h i
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ i
i : ℤ
⊢ QuasiIsoAt φ (n + i)

Tactic:
h (n + i)

Premises used: HAdd.hAdd
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
h : ∀ (i : ℤ), QuasiIsoAt φ i
i : ℤ
⊢ QuasiIsoAt φ (n + i)

Tactic:
exact h (n + i)

Premises used: HAdd.hAdd
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
inst_3 rw : QuasiIso φ
⊢ QuasiIso (K := Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) K)
    (CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) φ)

Tactic:
rw [quasiIso_shift_iff]

Premises used: CochainComplex.quasiIso_shift_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
n : ℤ
inst_3 : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
h :
  ∀ ⦃X Y : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)⦄ (f : X ⟶ Y),
    MorphismProperty.inverseImage (quasiIso C (up ℤ))
        (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) f ↔
      quasiIso C (up ℤ) f
⊢ Eq (α := MorphismProperty (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)))
    (MorphismProperty.inverseImage (quasiIso C (up ℤ))
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n))
    (quasiIso C (up ℤ))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
X Y : HomologicalComplex.{v_1, u_1, 0} C (up ℤ)
f : X ⟶ Y
⊢ MorphismProperty.inverseImage (quasiIso C (up ℤ))
      (CategoryTheory.shiftFunctor (HomologicalComplex.{v_1, u_1, 0} C (up ℤ)) n) f ↔
    quasiIso C (up ℤ) f

Tactic:
apply quasiIso_shift_iff

Premises used: CochainComplex.quasiIso_shift_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
n : ℤ
⊢ Eq (α := HomologicalComplex.{v_1, u_1, 0} C (up ℤ) ⥤ C) (Functor.shift (homologyFunctor C (up ℤ) 0) n)
    (homologyFunctor C (up ℤ) n)

Tactic:
rfl

Premises used: HomologicalComplex.homologyFunctor, CategoryTheory.Functor.shift, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ i' = i + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ i + 1 = j

Tactic:
simp only [next] at hj hj'

Premises used: CochainComplex.next
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
hj₁ : i + 1 = j
⊢ i' + 1 = j'

Tactic:
simp only [next] at hj hj'

Premises used: CochainComplex.next
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
⊢ i' = i + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj : i + 1 = j
hj' : i' + 1 = j'
obtain :
  ∀ (hi' : n + i = i + n) (hj' : i + n + 1 = j'), (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) j' = 0
⊢ (f ≫ (K.shiftFunctorObjXIso n i i' ⋯).hom) ≫ K.d i' j' = 0

Tactic:
obtain rfl : i' = i + n := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
⊢ j' = j + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : CategoryWithHomology.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
A : C
n i : ℤ
f : A ⟶ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).X i
j : ℤ
hf : f ≫ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).d i j = 0
j' : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j'
obtain :
  ∀ (hj' : i + n + 1 = j + n),
    Eq (α := A ⟶ K.X (j + n)) ((f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) (j + n)) 0
⊢ (f ≫ (K.shiftFunctorObjXIso n i (i + n) ⋯).hom) ≫ K.d (i + n) j' = 0

Tactic:
obtain rfl : j' = j + n := by lia

Premises used: rfl