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

Goal state before:
pp: case refine_4
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
      ((shiftFunctor C (-1)).map o.m₃ ≫ (shiftFunctor C (-1)).map ((shiftFunctor C 1).map v₂₃)) ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₂ =
    v₁₃ ≫ u₁₂

Tactic:
← Functor.map_comp,

Goal state after:
case refine_4
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
      (shiftFunctor C (-1)).map (o.m₃ ≫ (shiftFunctor C 1).map v₂₃) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₂ =
    v₁₃ ≫ u₁₂
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: case refine_4
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂) ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₂ =
    v₁₃ ≫ u₁₂

Tactic:
← Functor.map_comp,

Goal state after:
case refine_4
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map (v₁₃ ≫ u₁₂)) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₂ =
    v₁₃ ≫ u₁₂
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (commShiftIso F' a).hom.app (L.obj X) =
    F'.map ((commShiftIso L a).inv.app X) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X) ≫
        (commShiftIso F a).hom.app X ≫ (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)

Tactic:
by
  apply commShiftOfLocalization.iso_hom_app

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.shift n₀).map T.mor₁ ≫ (F.shift n₀).map T.mor₂ = 0

Tactic:
← Functor.map_comp,

Goal state after:
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.shift n₀).map (T.mor₁ ≫ T.mor₂) = 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 Q : ObjectProperty C
⊢ P.extensionProduct Q.isoClosure = P.extensionProduct Q

Tactic:
refine le_antisymm ?_ (monotone_extensionProduct_right _ Q.le_isoClosure)

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
⊢ P.extensionProduct Q.isoClosure ≤ P.extensionProduct Q
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: 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 Q R : ObjectProperty C
inst✝ : IsTriangulated C
X : C
⊢ (P.extensionProduct Q).extensionProduct R X → P.extensionProduct (Q.extensionProduct R) X

Tactic:
intro ⟨Y, C, f, g, h, hT, ⟨A, B, f', g', h', hT', hP, hQ⟩, hR⟩

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 Q R : ObjectProperty C✝
inst✝ : IsTriangulated C✝
X Y C : C✝
f : Y ⟶ X
g : X ⟶ C
h : C ⟶ (shiftFunctor C✝ 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
A B : C✝
f' : A ⟶ Y
g' : Y ⟶ B
h' : B ⟶ (shiftFunctor C✝ 1).obj A
hT' : Triangle.mk f' g' h' ∈ distinguishedTriangles
hP : P A
hQ : Q B
hR : R C
⊢ P.extensionProduct (Q.extensionProduct R) X
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case a
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.extensionProduct Q ≤ P.retractClosure.extensionProduct Q.retractClosure

Tactic:
grw [monotone_extensionProduct_right _ (le_retractClosure Q),
      monotone_extensionProduct_left _ (le_retractClosure P)]

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

Goal state before:
pp: case succ
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✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
⊢ P.extensionProductIter (n + m + 1) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))

Tactic:
extensionProductIter_succ',

Goal state after:
case succ
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✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
⊢ (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case succ
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✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
⊢ (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct (P.extensionProductIter (m + 1))

Tactic:
extensionProductIter_succ',

Goal state after:
case succ
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✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
m : ℕ
hm : P.extensionProductIter (n + m) = (P.extensionProductIter n').extensionProduct (P.extensionProductIter m)
⊢ (P.extensionProductIter (n + m)).extensionProduct P =
    (P.extensionProductIter n').extensionProduct ((P.extensionProductIter m).extensionProduct P)
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 ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
h : P T.obj₁
⊢ P.trW T.mor₂

Tactic:
trW_iff'

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 : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
h : P T.obj₁
⊢ ∃ X f h, ∃ (_ : Triangle.mk f T.mor₂ h ∈ distinguishedTriangles), P X
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)) (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom

Tactic:
intro f

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 : Arrow (HomotopyCategory C c)
⊢ ∀ (g : Arrow (HomotopyCategory C c)) (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Category.{v_4, u_4} E'
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
inst✝² : HasShift E' A
F G✝ H : SingleFunctors C D A
G : D ⥤ E
G' : E ⥤ E'
inst✝¹ : G.CommShift A
inst✝ : G'.CommShift A
n a a' : A
ha' : n + a = a'
X : C
⊢ ((((F.postcomp G).postcomp G').shiftIso n a a' ha').hom ≫ ((F.functor a).associator G G').hom).app X =
    (whiskerRight ((F.functor a').associator G G').hom (shiftFunctor E' n) ≫
          ((F.postcomp (G ⋙ G')).shiftIso n a a' ha').hom).app
      X

Tactic:
simp [Functor.commShiftIso_comp_inv_app]

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:
by
    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.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 : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ (mappingCone.snd φ).v (p + -1) (p + -1) ⋯ ≫ (δ (m + 1) (m + 2) β).v (p + -1) q ⋯ +
      (m.negOnePow • (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq +
        (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ (δ m (m + 1) α).v p q hpq) =
    (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ (δ m (m + 1) α).v p q hpq +
        m.negOnePow • (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq +
      (mappingCone.snd φ).v (p + -1) (p + -1) ⋯ ≫ (δ (m + 1) (m + 2) β).v (p + -1) q ⋯

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind` -/

Goal state after:
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 : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ (mappingCone.snd φ).v (p + -1) (p + -1) ⋯ ≫ (δ (m + 1) (m + 2) β).v (p + -1) q ⋯ +
      (m.negOnePow • (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq +
        (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ (δ m (m + 1) α).v p q hpq) =
    (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ (δ m (m + 1) α).v p q hpq +
        m.negOnePow • (↑(mappingCone.fst φ)).v (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq +
      (mappingCone.snd φ).v (p + -1) (p + -1) ⋯ ≫ (δ (m + 1) (m + 2) β).v (p + -1) q ⋯
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 ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ (δ n n' α).v p q hpq ≫ (mappingCone.inl φ).v q (q + -1) ⋯ +
      (-(δ m n β).v p (q + -1) ⋯ ≫ (mappingCone.inr φ).f (q + -1) +
        -α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ (mappingCone.inr φ).f (q + -1)) =
    (δ n n' α).v p q hpq ≫ (mappingCone.inl φ).v q (q + -1) ⋯ -
      ((δ m n β).v p (q + -1) ⋯ ≫ (mappingCone.inr φ).f (q + -1) +
        α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ (mappingCone.inr φ).f (q + -1))

Tactic:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
  canonicalizer; a minimization would help. The original proof was: `grind` -/

Goal state after:
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 ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ (δ n n' α).v p q hpq ≫ (mappingCone.inl φ).v q (q + -1) ⋯ +
      (-(δ m n β).v p (q + -1) ⋯ ≫ (mappingCone.inr φ).f (q + -1) +
        -α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ (mappingCone.inr φ).f (q + -1)) =
    (δ n n' α).v p q hpq ≫ (mappingCone.inl φ).v q (q + -1) ⋯ -
      ((δ m n β).v p (q + -1) ⋯ ≫ (mappingCone.inr φ).f (q + -1) +
        α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ (mappingCone.inr φ).f (q + -1))
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 ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h =
    (DerivedCategory.homologyFunctor C 0).shiftMap
        (DerivedCategory.Q.map T.mor₃ ≫ (Functor.commShiftIso DerivedCategory.Q 1).hom.app T.obj₁) n₀ n₁ ⋯ ≫
      (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁

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

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ homologyδOfTriangle T n₀ n₁ h =
    ((DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫
        (homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯ ≫
          (DerivedCategory.homologyFunctorFactors C n₁).inv.app T.obj₁) ≫
      (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁
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.symm
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.Rel i j
⊢ (f.f i).unop ≫ X✝.unopSymm.d i j = Y✝.unopSymm.d i j ≫ (f.f j).unop

Tactic:
simp only [unopSymm_d, ← unop_comp, f.comm]

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₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv

Tactic:
← Functor.map_comp,

Goal state after:
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₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
        ((mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv
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₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
        ((mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv

Tactic:
← Functor.map_comp,

Goal state after:
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₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
      (map (f ≫ g) g f (𝟙 X₃) ⋯ ≫ (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv
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₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
      (map (f ≫ g) g f (𝟙 X₃) ⋯ ≫ (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv

Tactic:
← Functor.map_comp,

Goal state after:
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₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
      (map (f ≫ g) g f (𝟙 X₃) ⋯ ≫ (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
      (inr (map f (f ≫ g) (𝟙 X₁) g ⋯) ≫ (mappingConeCompHomotopyEquiv f g).inv)