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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ ((lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map
          ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫
            (Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X) ≫
              (functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
Functor.map_comp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ ((lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
          (lift r F hF).map
            ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X) ≫
              (functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ ((lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
          (lift r F hF).map
            ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X) ≫
              (functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
Functor.map_comp,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ ((lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
          (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
            (lift r F hF).map ((functor r).map ((shiftFunctorAdd C a b).inv.app X))) ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorAdd (Quotient r) a b).hom.app ((functor r).obj X)) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map ((LiftCommShift.iso F r hF a).hom.app ((functor r).obj X)) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ (ComplexShape.up ℤ).Rel (i + n) (i + 1 + n)

Tactic:
dsimp; lia

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ (ComplexShape.up ℤ).Rel (i - 1 + n) (i + n)

Tactic:
dsimp; lia

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
⊢ ∀ (X : D),
    (Induced.add F s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom.app X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
by
        suffices (Induced.add F s i (m₁ + m₂) m₃).hom ≫
            whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
            eqToHom (by rw [add_assoc]) ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫
              whiskerLeft (s m₁) (Induced.add F s i m₂ m₃).hom by
          intro X
          simpa using NatTrans.congr_app this X
        apply ((whiskeringLeft C D D).obj F).map_injective
        ext X
        dsimp
        have eq := F.congr_map (shiftFunctorAdd'_assoc_hom_app
          m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl X)
        simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at eq
        simp only [Functor.comp_obj, Functor.map_comp, shiftFunctorAdd',
          Iso.trans_hom, eqToIso.hom, NatTrans.comp_app, eqToHom_app,
          Category.assoc] at eq
        rw [← cancel_mono ((s m₃).map ((s m₂).map ((i m₁).hom.app X)))]
        simp only [Induced.add_hom_app_obj, Category.assoc, Functor.map_comp]
        slice_lhs 4 5 =>
          erw [← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]
        erw [Category.id_comp]
        slice_lhs 6 7 =>
          erw [← Functor.map_comp, ← Functor.map_comp, Iso.inv_hom_id_app,
            (s m₂).map_id, (s m₃).map_id]
        erw [Category.comp_id, ← NatTrans.naturality_assoc, reassoc_of% eq,
          dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃).symm]
        simp only [Functor.comp_obj, eqToHom_map, eqToHom_app, NatTrans.naturality_assoc,
          Induced.add_hom_app_obj, Functor.comp_map, Category.assoc, Iso.inv_hom_id_app_assoc,
          eqToHom_trans_assoc, eqToHom_refl, Category.id_comp, Category.comp_id,
          ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
⊢ (γ.comp γ' hnm).rightUnshift nm' hnm' = γ.comp (γ'.rightUnshift m' hm') ⋯

Tactic:
by
  ext p q hpq
  rw [(γ.comp γ' hnm).rightUnshift_v nm' hnm' p q hpq (p + n + m) (by lia),
    γ.comp_v γ' hnm p (p + n) (p + n + m) rfl rfl,
    comp_v _ _ (show n + m' = nm' by lia) p (p + n) q (by lia) (by lia),
    γ'.rightUnshift_v m' hm' (p + n) q (by lia) (p + n + m) rfl, assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ n.negOnePow •
      ((CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) =
    n.negOnePow •
      (CategoryTheory.shiftFunctor C n).map (X✝.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map f.hom₁) ≫
        (shiftFunctorComm C 1 n).hom.app Y✝.obj₁

Tactic:
Functor.map_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ n.negOnePow •
      ((CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) =
    n.negOnePow •
      ((CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫
          (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C 1).map f.hom₁)) ≫
        (shiftFunctorComm C 1 n).hom.app Y✝.obj₁
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
A B : J ⥤ Triangle C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₁Toπ₂ ≫ iso₂.inv = iso₁.inv ≫ A.whiskerLeft π₁Toπ₂

Tactic:
simp only [← cancel_epi iso₁.hom, ← reassoc_of% comm₁,
          Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫
        (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁ ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        (CategoryTheory.shiftFunctor C b).map
            ((CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)

Tactic:
Functor.map_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctor C (a + b)).map T.mor₃ ≫
        (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁ ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
        ((CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₃) ≫
            (CategoryTheory.shiftFunctor C b).map ((shiftFunctorComm C 1 a).hom.app T.obj₁)) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁)
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.3 = 0 ↔ Epi T.mor₁
⊢ T.mor₂ = 0 ↔ Epi T.mor₁

Tactic:
rw [← h, IsIso.comp_right_eq_zero]

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

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✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₁) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
        ((triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a) ≫
      (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₂

Tactic:
Functor.map_comp,

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✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₁) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) =
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a)) ≫
      (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app K₂
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
⊢ g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π (fun j ↦ (T j).obj₃) j = 0

Tactic:
← reassoc_of% hg,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
⊢ f ≫ φ'.hom₃ ≫ Pi.π (fun j ↦ (T j).obj₃) j = 0
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

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
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
inst✝² : HasShift D M
G : Type u_5
inst✝¹ : AddGroup G
inst✝ : HasShift C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ 𝟙 (F.obj ((shiftFunctor C a).obj ((shiftFunctor C (m + n)).obj X))) ≫
      F.map ((shiftFunctorAdd' C (m + n) a a'' ⋯).inv.app X) =
    F.map ((shiftFunctor C a).map ((shiftFunctorAdd C m n).hom.app X)) ≫
      𝟙 (F.obj ((shiftFunctor C a).obj ((shiftFunctor C n).obj ((shiftFunctor C m).obj X)))) ≫
        (𝟙 (F.obj ((shiftFunctor C a).obj ((shiftFunctor C n).obj ((shiftFunctor C m).obj X)))) ≫
            F.map ((shiftFunctorAdd' C n a a' ha').inv.app ((shiftFunctor C m).obj X))) ≫
          𝟙 (F.obj ((shiftFunctor C a').obj ((shiftFunctor C m).obj X))) ≫
            F.map ((shiftFunctorAdd' C m a' a'' ha'').inv.app X)

Tactic:
simp only [id_comp, ← Functor.map_comp]

Goal state after:
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
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
inst✝² : HasShift D M
G : Type u_5
inst✝¹ : AddGroup G
inst✝ : HasShift C G
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ F.map ((shiftFunctorAdd' C (m + n) a a'' ⋯).inv.app X) =
    F.map
      ((shiftFunctor C a).map ((shiftFunctorAdd C m n).hom.app X) ≫
        (shiftFunctorAdd' C n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫
          (shiftFunctorAdd' C m a' a'' ha'').inv.app X)
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (lift φ).map f.toPath = φ.map f

Tactic:
by
  dsimp [Quiver.Hom.toPath, lift]
  simp

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

Goal state before:
pp: case refine_2
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₂₃
⊢ w₁₂ ≫
      (shiftFunctor C 1).map
        ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₂ ≫
          (shiftFunctor C (-1)).map o.m₁ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₁₃) =
    u₂₃ ≫ w₁₃

Tactic:
Functor.map_comp,

Goal state after:
case refine_2
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₂₃
⊢ w₁₂ ≫
      (shiftFunctor C 1).map ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₂) ≫
        (shiftFunctor C 1).map ((shiftFunctor C (-1)).map o.m₁ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₁₃) =
    u₂₃ ≫ w₁₃