mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ ((ofInv s hs).comp₀ (ofHom W s) (ofHom W (𝟙 Y))).s ≫ 𝟙 Y = (ofHom W (𝟙 ((Q W).obj Y))).s ≫ 𝟙 Y

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ ((ofInv s hs).comp₀ (ofHom W s) (ofHom W (𝟙 Y))).f ≫ 𝟙 Y = (ofHom W (𝟙 ((Q W).obj Y))).f ≫ 𝟙 Y

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj φ.left
H : Triangle.mk φ.hom g h ∈ distinguishedTriangles
⊢ (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
          (L.map h ≫ (Functor.commShiftIso L 1).hom.app φ.left ≫ (shiftFunctor D 1).map (Arrow.Hom.left e.hom))).mor₂ ≫
      (Iso.refl
          (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
              (L.map h ≫
                (Functor.commShiftIso L 1).hom.app φ.left ≫ (shiftFunctor D 1).map (Arrow.Hom.left e.hom))).obj₃).hom =
    (Arrow.rightFunc.mapIso e.symm).hom ≫ (L.mapTriangle.obj (Triangle.mk φ.hom g h)).mor₂

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
⊢ f = e.inv.app X ≫ (e.hom.app X ≫ f ≫ e.inv.app Y) ≫ e.hom.app Y

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
⊢ ((F.isoShift n₀).app T.obj₁).hom ≫
      { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
          f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }.f =
    ((shortComplexOfDistTriangle ((shiftFunctor (Triangle C) n₀).obj T) ⋯).map F).f ≫
      (n₀.negOnePow • (F.isoShift n₀).app T.obj₂).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
⊢ (n₀.negOnePow • (F.isoShift n₀).app T.obj₂).hom ≫
      { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
          f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }.g =
    ((shortComplexOfDistTriangle ((shiftFunctor (Triangle C) n₀).obj T) ⋯).map F).g ≫ ((F.isoShift n₀).app T.obj₃).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (Iso.refl
          { X₁ := (F.shift n₀).obj T.rotate.obj₁, X₂ := (F.shift n₀).obj T.rotate.obj₂,
              X₃ := (F.shift n₀).obj T.rotate.obj₃, f := (F.shift n₀).map T.rotate.mor₁,
              g := (F.shift n₀).map T.rotate.mor₂, zero := ⋯ }.X₁).hom ≫
      { X₁ := (F.shift n₀).obj T.obj₂, X₂ := (F.shift n₀).obj T.obj₃, X₃ := (F.shift n₁).obj T.obj₁,
          f := (F.shift n₀).map T.mor₂, g := F.homologySequenceδ T n₀ n₁ h, zero := ⋯ }.f =
    { X₁ := (F.shift n₀).obj T.rotate.obj₁, X₂ := (F.shift n₀).obj T.rotate.obj₂, X₃ := (F.shift n₀).obj T.rotate.obj₃,
          f := (F.shift n₀).map T.rotate.mor₁, g := (F.shift n₀).map T.rotate.mor₂, zero := ⋯ }.f ≫
      (Iso.refl
          { X₁ := (F.shift n₀).obj T.rotate.obj₁, X₂ := (F.shift n₀).obj T.rotate.obj₂,
              X₃ := (F.shift n₀).obj T.rotate.obj₃, f := (F.shift n₀).map T.rotate.mor₁,
              g := (F.shift n₀).map T.rotate.mor₂, zero := ⋯ }.X₂).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (Iso.refl
          { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
              X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
              g := (F.shift n₁).map T.invRotate.mor₂, zero := ⋯ }.X₂).hom ≫
      { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
          f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ }.g =
    { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
          X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
          g := (F.shift n₁).map T.invRotate.mor₂, zero := ⋯ }.g ≫
      (Iso.refl
          { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
              X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
              g := (F.shift n₁).map T.invRotate.mor₂, zero := ⋯ }.X₃).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h✝ : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h✝ ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h✝) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
n : ℤ
⊢ n = n - 1 + 1

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
G : C ⥤ A
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n a a' : M
ha' : n + a = a'
X : C
⊢ ((L.associator (shiftFunctor D n) (F' a)).symm ≪≫
            isoWhiskerRight (commShiftIso L n).symm (F' a) ≪≫
              (shiftFunctor C n).associator L (F' a) ≪≫
                (shiftFunctor C n).isoWhiskerLeft (e' a) ≪≫ G.shiftIso n a a' ha' ≪≫ (e' a').symm).hom.app
      X =
    (F' a).map ((commShiftIso L n).inv.app X) ≫
      (e' a).hom.app ((shiftFunctor C n).obj X) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X

Tactic:
by simp

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
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle C
hT : T ∈ distinguishedTriangles
X₁ : C
h₁ : P X₁
e₁ : T.obj₁ ≅ X₁
X₃ : C
h₃ : P X₃
e₃ : T.obj₃ ≅ X₃
⊢ (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom) (e₃.inv ≫ T.mor₃ ≫ (shiftFunctor C 1).map e₁.hom)).mor₁ ≫
      (Iso.refl
          (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom)
              (e₃.inv ≫ T.mor₃ ≫ (shiftFunctor C 1).map e₁.hom)).obj₂).hom =
    e₁.symm.hom ≫ T.mor₁

Tactic:
by simp

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
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle C
hT : T ∈ distinguishedTriangles
X₁ : C
h₁ : P X₁
e₁ : T.obj₁ ≅ X₁
X₃ : C
h₃ : P X₃
e₃ : T.obj₃ ≅ X₃
⊢ (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom) (e₃.inv ≫ T.mor₃ ≫ (shiftFunctor C 1).map e₁.hom)).mor₂ ≫
      e₃.symm.hom =
    (Iso.refl
          (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom)
              (e₃.inv ≫ T.mor₃ ≫ (shiftFunctor C 1).map e₁.hom)).obj₂).hom ≫
      T.mor₂

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 0 0 1).HasHomology
inst✝ : (sc' L 0 0 1).HasHomology
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 0 0 1).HasHomology
inst✝ : (sc' L 0 0 1).HasHomology
⊢ (ComplexShape.up ℕ).next 0 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : ChainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 1 0 0).HasHomology
inst✝ : (sc' L 1 0 0).HasHomology
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : ChainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 1 0 0).HasHomology
inst✝ : (sc' L 1 0 0).HasHomology
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by simp

Goal state after:
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'
K : CochainComplex C ℤ
⊢ (n.negOnePow • (shiftEval C n i i' hi).app K).hom ≫ ((shortComplexFunctor' C (up ℤ) i' j' k').obj K).f =
    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).obj K).f ≫
      ((shiftEval C n j j' hj).app K).hom

Tactic:
by simp

Goal state after:
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'
K : CochainComplex C ℤ
⊢ ((shiftEval C n j j' hj).app K).hom ≫ ((shortComplexFunctor' C (up ℤ) i' j' k').obj K).g =
    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ shortComplexFunctor' C (up ℤ) i j k).obj K).g ≫
      (n.negOnePow • (shiftEval C n k k' hk).app K).hom

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: 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)).τ₁

Tactic:
simp [one_smul, shiftFunctorZero_hom_app_f]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: 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)).τ₂

Tactic:
simp [one_smul, shiftFunctorZero_hom_app_f]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: 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)).τ₃

Tactic:
simp [one_smul, shiftFunctorZero_hom_app_f]

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
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : HasShift E ℤ
P : ObjectProperty C
X' X Y : C
e : X' ⟶ X
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).mor₁ ≫
      (Iso.refl (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).obj₂).hom =
    (asIso e).hom ≫ (Triangle.mk f g h).mor₁

Tactic:
by simp

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
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝² : Pretriangulated D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : HasShift E ℤ
P : ObjectProperty C
X' X Y : C
e : X' ⟶ X
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).mor₂ ≫
      (Iso.refl (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).obj₃).hom =
    (Iso.refl (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).obj₂).hom ≫ (Triangle.mk f g h).mor₂

Tactic:
by simp

Goal state after:
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 j : ℤ
h : n + i = j
⊢ IsIso (homologyMap ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i) ↔ IsIso (homologyMap φ j)

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

Goal state after:
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
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K : HomologicalComplex C c
i : ι
⊢ (((Quotient.functor (homotopic C c)).associator Qh (homologyFunctor C c i)).symm ≪≫
            Functor.isoWhiskerRight (quotientCompQhIso C c) (homologyFunctor C c i) ≪≫
              homologyFunctorFactors C c i ≪≫ (HomotopyCategory.homologyFunctorFactors C c i).symm).hom.app
      K =
    (homologyFunctor C c i).map ((quotientCompQhIso C c).hom.app K) ≫
      (homologyFunctorFactors C c i).hom.app K ≫ (HomotopyCategory.homologyFunctorFactors C c i).inv.app K

Tactic:
by simp

Goal state after:
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
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K : HomologicalComplex C c
i : ι
⊢ (((Quotient.functor (homotopic C c)).associator Qh (homologyFunctor C c i)).symm ≪≫
            Functor.isoWhiskerRight (quotientCompQhIso C c) (homologyFunctor C c i) ≪≫
              homologyFunctorFactors C c i ≪≫ (HomotopyCategory.homologyFunctorFactors C c i).symm).inv.app
      K =
    (HomotopyCategory.homologyFunctorFactors C c i).hom.app K ≫
      (homologyFunctorFactors C c i).inv.app K ≫ (homologyFunctor C c i).map ((quotientCompQhIso C c).inv.app K)

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
inst✝ : CategoryWithHomology C
n : ℤ
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso mn a a'' ⋯ =
    (F.functor a'').isoWhiskerLeft (shiftFunctorAdd' D m n mn hnm) ≪≫
      ((F.functor a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
        isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor D n) ≪≫ F.shiftIso n a a' ha'

Tactic:
by
  subst hnm
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]

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
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X Y : C
φ : P.trW.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj φ.X'
H : Triangle.mk φ.s f g ∈ distinguishedTriangles
mem : P Z
Y' : C
s' : Y ⟶ Y'
f' : Y' ⟶ Z
mem' : Triangle.mk s' f' (g ≫ (shiftFunctor C 1).map φ.f) ∈ distinguishedTriangles
⊢ (Triangle.mk φ.s f g).mor₃ ≫ (shiftFunctor C 1).map φ.f =
    𝟙 Z ≫ (Triangle.mk s' f' (g ≫ (shiftFunctor C 1).map φ.f)).mor₃

Tactic:
by simp

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
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
⊢ ∀ ⦃X' X Y : C⦄ (f₁ f₂ : X ⟶ Y) (s : X' ⟶ X), P.trW s → s ≫ f₁ = s ≫ f₂ → ∃ Y' t, ∃ (_ : P.trW t), f₁ ≫ t = f₂ ≫ t

Tactic:
rintro X' X Y f₁ f₂ s ⟨Z, g, h, H, mem⟩ hf₁
    have hf₂ : s ≫ (f₁ - f₂) = 0 := by rw [comp_sub, hf₁, sub_self]
    obtain ⟨q, hq⟩ := Triangle.yoneda_exact₂ _ H _ hf₂
    obtain ⟨Y', r, t, mem'⟩ := distinguished_cocone_triangle q
    refine ⟨Y', r, ?_, ?_⟩
    · exact ⟨_, _, _, rot_of_distTriang _ mem', P.le_shift _ _ mem⟩
    · have eq := comp_distTriang_mor_zero₁₂ _ mem'
      dsimp at eq
      rw [← sub_eq_zero, ← sub_comp, hq, assoc, eq, comp_zero]

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
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj Y
H : Triangle.mk φ.s f g ∈ distinguishedTriangles
mem : P Z
X' : C
f' : X' ⟶ X
h' : Z ⟶ (shiftFunctor C 1).obj X'
mem' : Triangle.mk f' (φ.f ≫ f) h' ∈ distinguishedTriangles
⊢ (Triangle.mk f' (φ.f ≫ f) h').mor₂ ≫ 𝟙 Z = φ.f ≫ (Triangle.mk φ.s f g).mor₂

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ f ≫ g = 𝟙 X₁ ≫ f ≫ g

Tactic:
by rw [id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ δ 0 1 (Cochain.ofHom (inr f)) = Int.negOnePow 1 • (Cochain.ofHom g).comp ↑0 ⋯

Tactic:
by simp

Goal state after: