mathlib-initiative/mathlib-tactics huggingface dataset:
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 Q : ObjectProperty C
⊢ P.retractClosure.extensionProduct Q.retractClosure ≤ (P.extensionProduct Q).retractClosure

Tactic:
intro X ⟨A, B, f₁, f₂, f₃, hT, ⟨A', hP, ⟨a₁, b₁, h₁⟩⟩, ⟨B', hQ, ⟨a₃, b₃, h₃⟩⟩⟩
  obtain ⟨X', g₁, g₂, hT'⟩ := distinguished_cocone_triangle₂ (b₃ ≫ f₃ ≫ a₁⟦(1 : ℤ)⟧')
  obtain ⟨a₂ : X ⟶ X', ha₁₂, ha₂₃⟩ :=
    complete_distinguished_triangle_morphism₂ _ _ hT hT' a₁ a₃ (by dsimp; grind)
  obtain ⟨b₂ : X' ⟶ X, hb₁₂, hb₂₃⟩ :=
    complete_distinguished_triangle_morphism₂ _ _ hT' hT b₁ b₃ (by dsimp; grind)
  dsimp at ha₁₂ ha₂₃ hb₁₂ hb₂₃
  refine ⟨X', ⟨_, _, _, _, _, hT', hP, hQ⟩, ⟨?_⟩⟩
  let φ := Triangle.homMk (Triangle.mk f₁ f₂ f₃) (Triangle.mk f₁ f₂ f₃) (𝟙 A)
    (a₂ ≫ b₂) (𝟙 B) (by dsimp; grind) (by dsimp; grind)
  haveI : IsIso (a₂ ≫ b₂) := isIso₂_of_isIso₁₃ φ hT hT (IsIso.id _) (IsIso.id _)
  exact ⟨a₂, b₂ ≫ inv (a₂ ≫ b₂), by grind⟩

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:
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:
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:
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:
simp

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

Goal state before:
pp: case zero
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
⊢ P.retractClosure.extensionProductIter 0 ≤ (P.extensionProductIter 0).retractClosure

Tactic:
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:
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:
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
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:
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
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:
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
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:
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
P Q : ObjectProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
⊢ P.trW f → Q.trW f

Tactic:
hf

Goal state after:
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 Q : ObjectProperty C
h : P ≤ Q
X Y : C
f : X ⟶ Y
hf : P.trW f
⊢ Q.trW 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
f g : Arrow (HomotopyCategory C c)
e : f ≅ g
⊢ quasiIso C c f.hom → quasiIso C c g.hom

Tactic:
hf

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
f g : Arrow (HomotopyCategory C c)
e : f ≅ g
hf : quasiIso C c f.hom
⊢ quasiIso C c g.hom
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:
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:
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).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:
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:
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:
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:
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 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:
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 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:
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.IsTriangulated
J : Type
x✝ : Finite J
X₁✝ X₂✝ : J → C
X₁ : HasProduct X₁✝
X₂ : HasProduct X₂✝
f : (j : J) → X₁✝ j ⟶ X₂✝ j
⊢ (∀ (j : J), P.isoClosure.trW (f j)) → P.isoClosure.trW (Limits.Pi.map f)

Tactic:
hf

Goal state after:
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.IsTriangulated
J : Type
x✝ : Finite J
X₁✝ X₂✝ : J → C
X₁ : HasProduct X₁✝
X₂ : HasProduct X₂✝
f : (j : J) → X₁✝ j ⟶ X₂✝ j
hf : ∀ (j : J), P.isoClosure.trW (f j)
⊢ P.isoClosure.trW (Limits.Pi.map f)
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:
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₃
⊢ δ (-1) 0 ((Cochain.ofHom f).comp (inl g) ⋯) = Cochain.ofHom ((f ≫ g) ≫ inr g)

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
⊢ -1 + 1 = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasBinaryBiproducts C
⊢ (triangle φ).rotate.mor₁ ≫ (Iso.refl (triangle φ).rotate.obj₂).hom =
    (Iso.refl (triangle φ).rotate.obj₁).hom ≫ (mappingCone.triangle φ).mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ 0 ≫ (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₂ =
    (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ (embeddingUpIntLE p).f (p - n).natAbs = n

Tactic:
simp

Goal state after:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ p - ↑(p - n).natAbs = n
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ (embeddingUpIntGE p).f (n - p).natAbs = n

Tactic:
simp

Goal state after:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ p + ↑(n - p).natAbs = n
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₃
⊢ MappingConeCompHomotopyEquiv.hom f g ≫ MappingConeCompHomotopyEquiv.inv f g = 𝟙 (mappingCone g)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex V c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ ((𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
            (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom).unop.f
      x =
    ((Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
            (opFunctor V c ⋙ opInverse V c).map f).unop.f
      x

Tactic:
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₃
inst✝ : HasZeroObject C
⊢ (mappingConeCompTriangleh f g).mor₂ ≫ (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).hom =
    (Iso.refl (mappingConeCompTriangleh f g).obj₂).hom ≫ (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₂

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X ⟶ Y
x : ι
⊢ ((𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
            (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom).unop.f
      x =
    ((Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
            (unopFunctor V c ⋙ unopInverse V c).map f).unop.f
      x

Tactic:
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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
⊢ (quotient C (ComplexShape.up ℤ)).map u₁₂ ≫ (Iso.refl { as := X₂ }).hom =
    (Iso.refl { as := X₁ }).hom ≫ (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₁

Tactic:
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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
⊢ (quotient C (ComplexShape.up ℤ)).map u₂₃ ≫ (Iso.refl { as := X₃ }).hom =
    (Iso.refl { as := X₂ }).hom ≫ (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₁

Tactic:
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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₃ ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app X₁) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((quotient C (ComplexShape.up ℤ)).map (𝟙 X₁)) =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₃ ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app X₁

Tactic:
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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ (quotient C (ComplexShape.up ℤ)).map (𝟙 X₃) ≫ (quotient C (ComplexShape.up ℤ)).map (mappingCone.inr u₂₃) =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.inr u₂₃)

Tactic:
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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ ((quotient C (ComplexShape.up ℤ)).mapTriangle.map β).hom₂ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj (mappingCone.triangle u₂₃)).mor₂ =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₂

Tactic:
dsimp [β]; simp

Goal state after: