mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hK : IsZero (K.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsZero (L.sc i).homology

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hK : IsZero (K.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) → IsZero (L.sc i).homology

case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hK : IsZero (K.sc i).homology
⊢ IsZero (L.sc i).homology → IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsZero (K.sc i).homology

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) → IsZero (K.sc i).homology

case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hL : IsZero (L.sc i).homology
⊢ IsZero (K.sc i).homology → IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ' i

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ' i

case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ' i → QuasiIsoAt (φ ≫ φ') i
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i ↔ QuasiIsoAt φ i

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ i

case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt φ i → QuasiIsoAt (φ ≫ φ') i
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
      (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
          (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom =
    (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
          (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
      (shortComplexFunctor' C (up ℤ) i' j' k').map f

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₁ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₂ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n i j k i' j' k' : ℤ
hi : n + i = i'
hj : n + j = j'
hk : n + k = k'
X✝ Y✝ : CochainComplex C ℤ
f : X✝ ⟶ Y✝
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).map f ≫
        (ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app Y✝) ((shiftEval C n j j' hj).app Y✝)
            (n.negOnePow • (shiftEval C n k k' hk).app Y✝) ⋯ ⋯).hom).τ₃ =
    ((ShortComplex.isoMk (n.negOnePow • (shiftEval C n i i' hi).app X✝) ((shiftEval C n j j' hj).app X✝)
            (n.negOnePow • (shiftEval C n k k' hk).app X✝) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C (up ℤ) i' j' k').map f).τ₃
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1) ↔
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1) →
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X) →
    ∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ (shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K =
    (shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₁ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₂ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₃ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₃
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn + a = a''

Tactic:
rw [← ha'', ← ha', ← add_assoc, hmn]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.isoClosure.trW f ↔ P.trW f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.isoClosure.trW f → P.trW f

case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.trW f → P.isoClosure.trW f
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ (shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K =
    (shortComplexFunctor C (up ℤ) a).map ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
      (shiftShortComplexFunctorIso C n a a' ha').hom.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
        (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K

Tactic:
ext

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₁ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₂ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₃ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₃
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ IsIso (Q.map f) ↔ HomologicalComplex.quasiIso C c f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ IsIso (Q.map f) → HomologicalComplex.quasiIso C c f

case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
⊢ HomologicalComplex.quasiIso C c f → IsIso (Q.map f)
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) ↔ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) → (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f)

case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ (HomologicalComplex.quasiIso C c).map (quotient C c) ((quotient C c).map f) → quasiIso C c ((quotient C c).map f)
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (∀ (i : ℤ), QuasiIsoAt φ (n + i)) ↔ ∀ (i : ℤ), QuasiIsoAt φ i

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (∀ (i : ℤ), QuasiIsoAt φ (n + i)) → ∀ (i : ℤ), QuasiIsoAt φ i

case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (∀ (i : ℤ), QuasiIsoAt φ i) → ∀ (i : ℤ), QuasiIsoAt φ (n + i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n : ℤ
⊢ (quasiIso C (up ℤ)).inverseImage (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n) = quasiIso C (up ℤ)

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n : ℤ
X✝ Y✝ : HomologicalComplex C (up ℤ)
f✝ : X✝ ⟶ Y✝
⊢ (quasiIso C (up ℤ)).inverseImage (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n) f✝ ↔
    quasiIso C (up ℤ) f✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0

Tactic:
apply (one_smul (M := ℤˣ) _).symm.trans _

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ 1 • (f ≫ 𝟙 (K.X (i + n))) ≫ K.d (i + n) (j + n) = 0
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ P.trW T.mor₁ ↔ P T.obj₃

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ P.trW T.mor₁ → P T.obj₃

case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ P T.obj₃ → P.trW T.mor₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X Y : C
f : X ⟶ Y
ha' : n + a = a + n
⊢ (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map f ≫
      (Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom =
    (Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom ≫ (single C (ComplexShape.up ℤ) a).map f

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n a : ℤ
X Y : C
f : X ⟶ Y
ha' : n + a = a + n
⊢ ((single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map f ≫
          (Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom).f
      a =
    ((Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯).hom ≫ (single C (ComplexShape.up ℤ) a).map f).f a
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
a : ℤ
⊢ NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯ =
    (single C (ComplexShape.up ℤ) a).isoWhiskerLeft (shiftFunctorZero (CochainComplex C ℤ) ℤ)

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
a : ℤ
x✝ : C
⊢ ((NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯).hom.app x✝).f a =
    (((single C (ComplexShape.up ℤ) a).isoWhiskerLeft (shiftFunctorZero (CochainComplex C ℤ) ℤ)).hom.app x✝).f a
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯ =
    (single C (ComplexShape.up ℤ) a'').isoWhiskerLeft (shiftFunctorAdd (CochainComplex C ℤ) m n) ≪≫
      ((single C (ComplexShape.up ℤ) a'').associator (CategoryTheory.shiftFunctor (CochainComplex C ℤ) m)
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n)).symm ≪≫
        Functor.isoWhiskerRight (NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯)
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) ≪≫
          NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x✝ : C
⊢ ((NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯).hom.app x✝).f a =
    (((single C (ComplexShape.up ℤ) a'').isoWhiskerLeft (shiftFunctorAdd (CochainComplex C ℤ) m n) ≪≫
                ((single C (ComplexShape.up ℤ) a'').associator (CategoryTheory.shiftFunctor (CochainComplex C ℤ) m)
                      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n)).symm ≪≫
                  Functor.isoWhiskerRight (NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯)
                      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) ≪≫
                    NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯).hom.app
          x✝).f
      a
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ T ∈ distinguishedTriangles ↔ ∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ T ∈ distinguishedTriangles → ∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ (∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))) → T ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ IsIso (Qh.map f) → HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f → IsIso (Qh.map f)