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

Goal state before:
pp: case neg.h₀
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

Tactic:
simp

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

Goal state before:
pp: case pos
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ ((shortComplexFunctor C c i).obj K).g ≫ K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
X✝ Y✝ : Quotient r
f : Hom r X✝ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as),
    comp r (Quot.mk (HomRel.CompClosure r) (𝟙 X✝.as)) (Quot.mk (HomRel.CompClosure r) a) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
X✝ Y✝ : Quotient r
f : Hom r X✝ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as),
    comp r (Quot.mk (HomRel.CompClosure r) a) (Quot.mk (HomRel.CompClosure r) (𝟙 Y✝.as)) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₀ K ≫ π K = 𝟙 K

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
W✝ X✝ Y✝ Z✝ : Quotient r
f : Hom r W✝ X✝
g : Hom r X✝ Y✝
h : Hom r Y✝ Z✝
⊢ ∀ (a : Y✝.as ⟶ Z✝.as) (a_1 : X✝.as ⟶ Y✝.as) (a_2 : W✝.as ⟶ X✝.as),
    comp r (comp r (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_1))
        (Quot.mk (HomRel.CompClosure r) a) =
      comp r (Quot.mk (HomRel.CompClosure r) a_2)
        (comp r (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a))

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₀ K = ι₁ K ≫ π K ≫ ι₀ K

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₁ K ≫ 𝟙 K.cylinder = ι₁ K

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F

Tactic:
natTransLift_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ 𝟙 F = 𝟙 F
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r (𝟙 (functor r ⋙ G)) = 𝟙 G

Tactic:
natTransLift_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ 𝟙 G = 𝟙 G
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.Full
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
L : C ⥤ D
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.EssSurj
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.Full
inst✝ : L.EssSurj
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
X✝ Y✝ : HomologicalComplex V c
f₁✝ f₂✝ g₁✝ g₂✝ : X✝ ⟶ Y✝
h : Homotopy f₁✝ f₂✝
h' : Homotopy g₁✝ g₂✝
⊢ homotopic V c (f₁✝ + g₁✝) (f₂✝ + g₂✝)

Tactic:
exact ⟨Homotopy.add h h'⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
⊢ (quotient V c).map (Quot.out ((quotient V c).map f)) = (quotient V c).map f

Tactic:
simp

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomotopyCategory V c
f : C ⟶ D
g : D ⟶ E
⊢ (quotient V c).map (Quot.out f ≫ Quot.out g) = f ≫ g

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ 𝟙 ((quotient V c).obj C) = (quotient V c).map (𝟙 C)

Tactic:
(quotient V c).map_id

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ 𝟙 ((quotient V c).obj C) = 𝟙 ((quotient V c).obj C)
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ 𝟙 ((quotient V c).obj D) = (quotient V c).map (𝟙 D)

Tactic:
(quotient V c).map_id

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ 𝟙 ((quotient V c).obj D) = 𝟙 ((quotient V c).obj D)
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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
X : C
h :
  F.whiskerLeft (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom.app X =
    (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
simp

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
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
X : C
h :
  F.whiskerLeft (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv.app X =
    F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
simp

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).hom =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
            (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
              ((shiftFunctor C a).associator F (s b)).symm ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
                (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
                  ((shiftFunctor C a).associator F (s b)).symm ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom.app
      X =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)

Tactic:
simp

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
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
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).inv =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
            (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
              ((shiftFunctor C a).associator F (s b)).symm ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
                (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
                  ((shiftFunctor C a).associator F (s b)).symm ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv.app
      X =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
simp

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
n : ℤ
h : n = 0
X✝ Y✝ : CochainComplex C ℤ
x✝ : X✝ ⟶ Y✝
i✝ : ℤ
⊢ ((shiftFunctor C n).map x✝ ≫ (Hom.isoOfComponents (fun i ↦ Y✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom).f i✝ =
    ((Hom.isoOfComponents (fun i ↦ X✝.shiftFunctorObjXIso n i i ⋯) ⋯).hom ≫ (𝟭 (CochainComplex C ℤ)).map x✝).f i✝

Tactic:
simp

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
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
X✝ Y✝ : CochainComplex C ℤ
f✝ : X✝ ⟶ Y✝
i✝ : ℤ
⊢ ((shiftFunctor C n₁₂).map f✝ ≫ (Hom.isoOfComponents (fun i ↦ Y✝.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom).f
      i✝ =
    ((Hom.isoOfComponents (fun i ↦ X✝.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom ≫
          (shiftFunctor C n₁ ⋙ shiftFunctor C n₂).map f✝).f
      i✝

Tactic:
simp

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
n i i' : ℤ
hi : n + i = i'
⊢ ∀ {X Y : CochainComplex C ℤ} (f : X ⟶ Y),
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ eval C (ComplexShape.up ℤ) i).map f ≫ (XIsoOfEq Y ⋯).hom =
      (XIsoOfEq X ⋯).hom ≫ (eval C (ComplexShape.up ℤ) i').map f

Tactic:
simp

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
F : C ⥤ D
inst✝ : F.Additive
n : ℤ
K : HomologicalComplex C (ComplexShape.up ℤ)
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    K).X
                i)).hom ≫
          ((F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n).obj
                K).d
            i j =
        ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                K).d
            i j ≫
          (Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    K).X
                j)).hom

Tactic:
simp

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 (i + 1)

Tactic:
simp

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) i

Tactic:
simp

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
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)
h₂ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map (r • f))
⊢ (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    r •
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
        (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₁ ≫ (asIso f.hom₂).hom = (asIso f.hom₁).hom ≫ B.mor₁

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₂ ≫ (asIso f.hom₃).hom = (asIso f.hom₂).hom ≫ B.mor₂

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₃ ≫ (shiftFunctor C 1).map (asIso f.hom₁).hom = (asIso f.hom₃).hom ≫ B.mor₃

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
X : C
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (-(shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X✝.obj₁) ≫ f.hom₁ =
    -((shiftFunctor C (-1)).map X✝.mor₃ ≫ (shiftFunctor C (-1)).map ((shiftFunctor C 1).map f.hom₁)) ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Y✝.obj₁

Tactic:
simp

Goal state after:
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
X₁ X₂ : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X₁ X₂
⊢ (binaryProductTriangle X₁ X₂).mor₂ ≫ (Iso.refl (binaryProductTriangle X₁ X₂).obj₃).hom =
    (biprod.isoProd X₁ X₂).symm.hom ≫ (binaryBiproductTriangle X₁ X₂).mor₂

Tactic:
simp

Goal state after:
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
X₁ X₂ : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X₁ X₂
⊢ (binaryProductTriangle X₁ X₂).mor₃ ≫ (shiftFunctor C 1).map (Iso.refl (binaryProductTriangle X₁ X₂).obj₁).hom =
    (Iso.refl (binaryProductTriangle X₁ X₂).obj₃).hom ≫ (binaryBiproductTriangle X₁ X₂).mor₃

Tactic:
simp

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
T : Triangle C
⊢ ((shiftFunctor C 0).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₁).hom ≫ ((𝟭 (Triangle C)).obj T).mor₁

Tactic:
simp

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
T : Triangle C
⊢ ((shiftFunctor C 0).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorZero C ℤ).app T.obj₂).hom ≫ ((𝟭 (Triangle C)).obj T).mor₂

Tactic:
simp

Goal state after:
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.Shift.CommShift

Goal state before:
pp: case e_a.e_a
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
A✝ : Type u_4
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a b : A
X : C
⊢ (shiftFunctor E b).map
      ((commShiftIso H a).hom.app X ≫ (shiftFunctor E a).map (e.inv.app X) ≫ (commShiftIso G a).inv.app (F.obj X)) =
    (shiftFunctor E b).map (e.inv.app ((shiftFunctor C a).obj X) ≫ G.map ((OfComp.iso e a).hom.app X))

Tactic:
simp

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ m.negOnePow • a.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯ =
    a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯

Tactic:
rw [smul_comm]

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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
X✝ Y✝ : Triangle C
f✝ : X✝ ⟶ Y✝
⊢ ((shiftFunctor C n).map f✝ ≫
        (((shiftFunctor C n).obj Y✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj Y✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app Y✝.obj₃) ⋯ ⋯ ⋯).hom).hom₁ =
    ((((shiftFunctor C n).obj X✝).isoMk ((shiftFunctor C a ⋙ shiftFunctor C b).obj X✝)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₁)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₂)
            ((CategoryTheory.shiftFunctorAdd' C a b n h).app X✝.obj₃) ⋯ ⋯ ⋯).hom ≫
        (shiftFunctor C a ⋙ shiftFunctor C b).map f✝).hom₁

Tactic:
simp

Goal state after: