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

Goal state before:
pp: case neg
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : ¬c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
⊢ 0 = d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' + d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
]

Goal state after:
case neg
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{v_1, u_1} C₁
inst✝²² : Category.{v_2, u_2} C₂
inst✝²¹ : Category.{v_3, u_5} C₃
inst✝²⁰ : Category.{v_4, u_6} C₄
inst✝¹⁹ : Category.{v_6, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : ¬c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
⊢ 0 = d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' + d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsCofibrant X
f g : X ⟶ Y
⊢ mk f = mk g ↔ Relation.EqvGen LeftHomotopyRel f g

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsCofibrant X
f g : X ⟶ Y
⊢ mk f = mk g ↔ Relation.EqvGen LeftHomotopyRel f g
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : PathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : (trivialCofibrations C).MapFactorizationData (fibrations C) P.p :=
  (trivialCofibrations C).factorizationData (fibrations C) P.p
⊢ fibrations C
    { P := d.Z, p₀ := d.p ≫ prod.fst, p₁ := d.p ≫ prod.snd, ι := P.ι ≫ d.i, ι_p₀ := ⋯, ι_p₁ := ⋯,
        weakEquivalence_ι := ⋯ }.p

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : PathObject Y
f g : X ⟶ Y
h : P.RightHomotopy f g
d : (trivialCofibrations C).MapFactorizationData (fibrations C) P.p :=
  (trivialCofibrations C).factorizationData (fibrations C) P.p
⊢ fibrations C
    { P := d.Z, p₀ := d.p ≫ prod.fst, p₁ := d.p ≫ prod.snd, ι := P.ι ≫ d.i, ι_p₀ := ⋯, ι_p₁ := ⋯,
        weakEquivalence_ι := ⋯ }.p
Module: Mathlib.CategoryTheory.Localization.OfQuotient

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✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.ι
⊢ L.op.IsLocalization W.op

Tactic:
]

Goal state after:
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✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.ι
⊢ L.op.IsLocalization W.op
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ L.map f = L.map g

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ L.map f = L.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ WeakEquivalence P.ι

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ WeakEquivalence P.ι
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
inst✝ : Congruence r
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.ι
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
⊢ ∃ P x, W P.ι

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
inst✝ : Congruence r
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.ι
X Y : C
f₀ f₁ : X ⟶ Y
hf : r f₀ f₁
⊢ ∃ P x, W P.ι
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝ : RightHomotopyRel f g
P : PathObject Y
left✝ : P.IsGood
h : P.RightHomotopy f g
fac : (cofibrations C).MapFactorizationData (trivialFibrations C) P.ι :=
  (cofibrations C).factorizationData (trivialFibrations C) P.ι
P' : PathObject Y :=
  { P := fac.Z, p₀ := fac.p ≫ P.p₀, p₁ := fac.p ≫ P.p₁, ι := fac.i, ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
⊢ Fibration (fac.p ≫ P.p)

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝ : RightHomotopyRel f g
P : PathObject Y
left✝ : P.IsGood
h : P.RightHomotopy f g
fac : (cofibrations C).MapFactorizationData (trivialFibrations C) P.ι :=
  (cofibrations C).factorizationData (trivialFibrations C) P.ι
P' : PathObject Y :=
  { P := fac.Z, p₀ := fac.p ≫ P.p₀, p₁ := fac.p ≫ P.p₁, ι := fac.i, ι_p₀ := ⋯, ι_p₁ := ⋯, weakEquivalence_ι := ⋯ }
⊢ Fibration (fac.p ≫ P.p)
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ mk f = mk g ↔ Relation.EqvGen RightHomotopyRel f g

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsFibrant Y
f g : X ⟶ Y
⊢ mk f = mk g ↔ Relation.EqvGen RightHomotopyRel f g
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle Cᵒᵖ
hT : Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
⊢ P.op.isoClosure T.obj₂

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
T : Triangle Cᵒᵖ
hT : Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles
h₁ : P.op T.obj₁
h₃ : P.op T.obj₃
⊢ P.op.isoClosure T.obj₂
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulated
X Y : C
f : X ⟶ Y
Z : Cᵒᵖ
a : Opposite.op X ⟶ Z
b : Z ⟶ (shiftFunctor Cᵒᵖ 1).obj (Opposite.op Y)
h₁ : Triangle.mk f.op a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.op Z
⊢ ∃ X_1 f_1 h, ∃ (_ : Triangle.mk f_1 f h ∈ Pretriangulated.distinguishedTriangles), P X_1

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulated
X Y : C
f : X ⟶ Y
Z : Cᵒᵖ
a : Opposite.op X ⟶ Z
b : Z ⟶ (shiftFunctor Cᵒᵖ 1).obj (Opposite.op Y)
h₁ : Triangle.mk f.op a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.op Z
⊢ ∃ X_1 f_1 h, ∃ (_ : Triangle.mk f_1 f h ∈ Pretriangulated.distinguishedTriangles), P X_1
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj (Opposite.unop Y)
h₁ : Triangle.mk f.unop a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.unop Z
⊢ ∃ X_1 f_1 h, ∃ (_ : Triangle.mk f_1 f h ∈ Pretriangulated.distinguishedTriangles), P X_1

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
a : Opposite.unop X ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj (Opposite.unop Y)
h₁ : Triangle.mk f.unop a b ∈ Pretriangulated.distinguishedTriangles
h₂ : P.unop Z
⊢ ∃ X_1 f_1 h, ∃ (_ : Triangle.mk f_1 f h ∈ Pretriangulated.distinguishedTriangles), P X_1
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((cylinder K).X i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((cylinder K).X i)
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (commShiftIso G (m + n)).hom.app ((Φ a'').obj X) ≫
      (shiftFunctor E (m + n)).map ((hΦ a'').hom.app X) ≫
        ((F.functor a'').isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
                  ((F.functor a'').associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
                    isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor E n) ≪≫ F.shiftIso n a a' ha').hom.app
            X ≫
          (hΦ a).inv.app X =
    G.map ((shiftFunctorAdd D m n).hom.app ((Φ a'').obj X)) ≫
      G.map (𝟙 ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((Φ a'').obj X)))) ≫
        (commShiftIso G n).hom.app ((shiftFunctor D m).obj ((Φ a'').obj X)) ≫
          ((shiftFunctor E n).map ((commShiftIso G m).hom.app ((Φ a'').obj X)) ≫
              (shiftFunctor E n).map ((shiftFunctor E m).map ((hΦ a'').hom.app X)) ≫
                (shiftFunctor E n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫
                  (shiftFunctor E n).map ((hΦ a').inv.app X)) ≫
            (shiftFunctor E n).map ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X ≫ (hΦ a).inv.app X

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (commShiftIso G (m + n)).hom.app ((Φ a'').obj X) ≫
      (shiftFunctor E (m + n)).map ((hΦ a'').hom.app X) ≫
        ((F.functor a'').isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
                  ((F.functor a'').associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
                    isoWhiskerRight (F.shiftIso m a' a'' ha'') (shiftFunctor E n) ≪≫ F.shiftIso n a a' ha').hom.app
            X ≫
          (hΦ a).inv.app X =
    G.map ((shiftFunctorAdd D m n).hom.app ((Φ a'').obj X)) ≫
      G.map (𝟙 ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((Φ a'').obj X)))) ≫
        (commShiftIso G n).hom.app ((shiftFunctor D m).obj ((Φ a'').obj X)) ≫
          ((shiftFunctor E n).map ((commShiftIso G m).hom.app ((Φ a'').obj X)) ≫
              (shiftFunctor E n).map ((shiftFunctor E m).map ((hΦ a'').hom.app X)) ≫
                (shiftFunctor E n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫
                  (shiftFunctor E n).map ((hΦ a').inv.app X)) ≫
            (shiftFunctor E n).map ((hΦ a').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X ≫ (hΦ a).inv.app X
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((pathObject K).X i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((pathObject K).X i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
K L : CochainComplex C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst✝¹ : K.IsStrictlyGE n₁
inst✝ : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero ((mappingCone f).X i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
K L : CochainComplex C ℤ
f : K ⟶ L
n₁ n₂ n : ℤ
inst✝¹ : K.IsStrictlyGE n₁
inst✝ : L.IsStrictlyGE n₂
hn₁ : n < n₁
hn₂ : n ≤ n₂
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero ((mappingCone f).X i)
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹³ : Category.{u_5, u_1} C
inst✝¹² : Category.{u_6, u_2} D
inst✝¹¹ : Category.{u_7, u_3} E
A : Type u_4
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝⁷ : G.CommShift A
inst✝⁶ : G.Full
inst✝⁵ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : G.Additive
a : A
inst✝ : (F.functor a).Additive
⊢ (F.functor a).Additive

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹³ : Category.{u_5, u_1} C
inst✝¹² : Category.{u_6, u_2} D
inst✝¹¹ : Category.{u_7, u_3} E
A : Type u_4
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝⁷ : G.CommShift A
inst✝⁶ : G.Full
inst✝⁵ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : G.Additive
a : A
inst✝ : (F.functor a).Additive
⊢ (F.functor a).Additive
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝³³ : Category.{v_1, u_1} C₁
inst✝³² : Category.{v_2, u_2} C₂
inst✝³¹ : Category.{v_3, u_5} C₃
inst✝³⁰ : Category.{v_4, u_6} C₄
inst✝²⁹ : Category.{v_5, u_3} C₁₂
inst✝²⁸ : Category.{v_6, u_4} C₂₃
inst✝²⁷ : HasZeroMorphisms C₁
inst✝²⁶ : HasZeroMorphisms C₂
inst✝²⁵ : HasZeroMorphisms C₃
inst✝²⁴ : Preadditive C₁₂
inst✝²³ : Preadditive C₂₃
inst✝²² : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝²¹ : F₁₂.PreservesZeroMorphisms
inst✝²⁰ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁹ : G.Additive
inst✝¹⁸ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹⁷ : G₂₃.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁵ : F.PreservesZeroMorphisms
inst✝¹⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝¹³ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝¹² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹¹ : TotalComplexShape c₁₂ c₃ c₄
inst✝¹⁰ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁹ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁸ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝⁷ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝⁶ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝⁵ : DecidableEq ι₁₂
inst✝⁴ : DecidableEq ι₂₃
inst✝³ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝² : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝¹ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
      mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h =
    ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
      mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h

Tactic:
]

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

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
inst✝³ : Preadditive C
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
n : ℤ
K : CochainComplex C ℤ
q : ℤ
h✝ : K.IsStrictlyGE q
⊢ CochainComplex.plus C ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
n : ℤ
K : CochainComplex C ℤ
q : ℤ
h✝ : K.IsStrictlyGE q
⊢ CochainComplex.plus C ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj K)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

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
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj T.obj₁.as)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj T.obj₁.as)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

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
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj T.obj₂.as)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj T.obj₂.as)