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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ (shiftFunctorCompIsoId C p' p hp).hom.app X =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorCompIsoId C n' n hn).hom.app X

Tactic:
← cancel_mono ((shiftFunctorCompIsoId C p' p hp).inv.app X),

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ (shiftFunctorCompIsoId C p' p hp).hom.app X ≫ (shiftFunctorCompIsoId C p' p hp).inv.app X =
    ((shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
        (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorCompIsoId C n' n hn).hom.app X) ≫
      (shiftFunctorCompIsoId C p' p hp).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i : A
⊢ (shiftFunctorAdd' C i i (i + i) ⋯).symm ≪≫ shiftFunctorAdd' C i i (i + i) ⋯ =
    Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i)

Tactic:
Iso.symm_self_id

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i : A
⊢ Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i) = Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i)
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (single C c i)

Tactic:
intros

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroObject C
inst✝² : DecidableEq ι
i : ι
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ (single C c i)
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i : ι
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J (single C c i)

Tactic:
intros

Goal state after:
C : Type u_1
ι : Type u_2
J : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroObject C
inst✝² : DecidableEq ι
i : ι
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesColimitsOfShape J✝ (single C c i)
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝² : HasFiniteLimits C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits F
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesLimitsOfShape J (F.mapHomologicalComplex c)

Tactic:
intros

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝⁴ : HasFiniteLimits C
inst✝³ : F.PreservesZeroMorphisms
inst✝² : PreservesFiniteLimits F
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ (F.mapHomologicalComplex c)
Module: Mathlib.Algebra.Homology.HomologicalComplexAbelian

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝² : HasFiniteColimits C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesFiniteColimits F
⊢ ∀ (J : Type) [inst : SmallCategory J] [FinCategory J], PreservesColimitsOfShape J (F.mapHomologicalComplex c)

Tactic:
intros

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : HasZeroMorphisms C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasZeroMorphisms D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝⁴ : HasFiniteColimits C
inst✝³ : F.PreservesZeroMorphisms
inst✝² : PreservesFiniteColimits F
J✝ : Type
inst✝¹ : SmallCategory J✝
inst✝ : FinCategory J✝
⊢ PreservesColimitsOfShape J✝ (F.mapHomologicalComplex c)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
⊢ nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j ↦ hom i j ≫ g.f j

Tactic:
ext n
  dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
  simp only [Preadditive.add_comp, assoc, g.comm]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
h₁ : (γ₁.comp (↑(fst φ)) hij).v p (q + 1) ⋯ = (γ₂.comp (↑(fst φ)) hij).v p (q + 1) ⋯
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯

Tactic:
replace h₂ := Cochain.congr_v h₂ p q hpq

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
p q : ℤ
hpq : p + i = q
h₁ : (γ₁.comp (↑(fst φ)) hij).v p (q + 1) ⋯ = (γ₂.comp (↑(fst φ)) hij).v p (q + 1) ⋯
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : 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 : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
f : HomotopyEquiv X✝ Y✝
g : HomotopyEquiv Y✝ Z✝
⊢ homotopyEquivalences V c (f.hom ≫ g.hom)

Tactic:
exact ⟨f.trans g, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f✝ g : X ⟶ Y
f g₁ g₂ : X.as ⟶ Y.as
h₁₂ : HomRel.CompClosure r g₁ g₂
⊢ Quot.mk (HomRel.CompClosure r) (f + g₁) = Quot.mk (HomRel.CompClosure r) (f + g₂)

Tactic:
simp only [HomRel.compClosure_iff_self] at h₁₂
      erw [functor_map_eq_iff]
      exact hr _ _ _ _ (Congruence.equivalence.refl f) h₁₂

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 : ℤ
K : CochainComplex C ℤ
⊢ ∀ (i j k : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (ComplexShape.up ℤ).Rel j k → (n.negOnePow • K.d (i + n) (j + n)) ≫ (n.negOnePow • K.d (j + n) (k + n)) = 0

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
K : CochainComplex C ℤ
i✝ j✝ k✝ : ℤ
a✝¹ : (ComplexShape.up ℤ).Rel i✝ j✝
a✝ : (ComplexShape.up ℤ).Rel j✝ k✝
⊢ (n.negOnePow • K.d (i✝ + n) (j✝ + n)) ≫ (n.negOnePow • K.d (j✝ + n) (k✝ + n)) = 0
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 : ℤ
X✝ Y✝ : CochainComplex C ℤ
φ : X✝ ⟶ Y✝
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      φ.f (i + n) ≫
          { X := fun i ↦ Y✝.X (i + n), d := fun x x_1 ↦ n.negOnePow • Y✝.d (x + n) (x_1 + n), shape := ⋯,
                d_comp_d' := ⋯ }.d
            i j =
        { X := fun i ↦ X✝.X (i + n), d := fun x x_1 ↦ n.negOnePow • X✝.d (x + n) (x_1 + n), shape := ⋯,
                d_comp_d' := ⋯ }.d
            i j ≫
          φ.f (j + n)

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
X✝ Y✝ : CochainComplex C ℤ
φ : X✝ ⟶ Y✝
i✝ j✝ : ℤ
a✝ : (ComplexShape.up ℤ).Rel i✝ j✝
⊢ φ.f (i✝ + n) ≫
      { X := fun i ↦ Y✝.X (i + n), d := fun x x_1 ↦ n.negOnePow • Y✝.d (x + n) (x_1 + n), shape := ⋯, d_comp_d' := ⋯ }.d
        i✝ j✝ =
    { X := fun i ↦ X✝.X (i + n), d := fun x x_1 ↦ n.negOnePow • X✝.d (x + n) (x_1 + n), shape := ⋯, d_comp_d' := ⋯ }.d
        i✝ j✝ ≫
      φ.f (j✝ + n)
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 : ℤ
⊢ ∀ (X : CochainComplex C ℤ),
    { f := fun x ↦ (𝟙 X).f (x + n), comm' := ⋯ } =
      𝟙 { X := fun i ↦ X.X (i + n), d := fun x x_1 ↦ n.negOnePow • X.d (x + n) (x_1 + n), shape := ⋯, d_comp_d' := ⋯ }

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
X✝ : CochainComplex C ℤ
⊢ { f := fun x ↦ (𝟙 X✝).f (x + n), comm' := ⋯ } =
    𝟙 { X := fun i ↦ X✝.X (i + n), d := fun x x_1 ↦ n.negOnePow • X✝.d (x + n) (x_1 + n), shape := ⋯, d_comp_d' := ⋯ }
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 : ℤ
⊢ ∀ {X Y Z : CochainComplex C ℤ} (f : X ⟶ Y) (g : Y ⟶ Z),
    { f := fun x ↦ (f ≫ g).f (x + n), comm' := ⋯ } =
      { f := fun x ↦ f.f (x + n), comm' := ⋯ } ≫ { f := fun x ↦ g.f (x + n), comm' := ⋯ }

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n : ℤ
X✝ Y✝ Z✝ : CochainComplex C ℤ
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ { f := fun x ↦ (f✝ ≫ g✝).f (x + n), comm' := ⋯ } =
    { f := fun x ↦ f✝.f (x + n), comm' := ⋯ } ≫ { f := fun x ↦ g✝.f (x + n), comm' := ⋯ }
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),
    (shiftFunctor C n₁₂).map f ≫ (Hom.isoOfComponents (fun i ↦ Y.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom =
      (Hom.isoOfComponents (fun i ↦ X.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom ≫
        (shiftFunctor C n₁ ⋙ shiftFunctor C n₂).map f

Tactic:
intros

Goal state after:
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✝
⊢ (shiftFunctor C n₁₂).map f✝ ≫ (Hom.isoOfComponents (fun i ↦ Y✝.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom =
    (Hom.isoOfComponents (fun i ↦ X✝.shiftFunctorObjXIso n₁₂ i (i + n₂ + n₁) ⋯) ⋯).hom ≫
      (shiftFunctor C n₁ ⋙ shiftFunctor C n₂).map f✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((shiftFunctorAdd (CochainComplex C ℤ) a b).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
shiftFunctorAdd_hom_app_f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ (XIsoOfEq K ⋯).hom = (XIsoOfEq K ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ γ₁ γ₂ : Cochain K L n✝
n a : ℤ
⊢ ∀ (a_1 b : Cochain K L n), (a_1 + b).shift a = a_1.shift a + b.shift a

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ γ₁ γ₂ : Cochain K L n✝
n a : ℤ
a✝ b✝ : Cochain K L n
⊢ (a✝ + b✝).shift a = a✝.shift a + b✝.shift a
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
⊢ isoAdd' ⋯ (isoAdd' hab ea eb) ec = isoAdd' ⋯ ea (isoAdd' hbc eb ec)

Tactic:
by
  ext X
  have := NatTrans.naturality_2 ec.hom ((shiftFunctorAdd' C a b ab hab).app X)
  dsimp at this ⊢
  simp only [isoAdd'_hom_app, Category.assoc]
  rw [← NatTrans.naturality_assoc, ← this, Category.assoc, ← F.map_comp_assoc,
    shiftFunctorAdd'_assoc_hom_app a b c ab bc abc hab hbc h,
    Functor.map_comp_assoc, Category.assoc]
  simp_rw [← Functor.map_comp_assoc]
  simp [shiftFunctorAdd'_assoc_inv_app a b c ab bc abc hab hbc h]

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 n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯) ≫
        L.d (p + n') q +
      m'.negOnePow •
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).d p (p + 1) ≫
          ((a * n' + a * (a - 1) / 2).negOnePow •
            (K.shiftFunctorObjXIso a (p + 1) (p + 1 + a) ⋯).hom ≫ γ.v (p + 1 + a) q ⋯) =
    a.negOnePow •
      (a * m' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫
          (γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q + m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯)

Tactic:
simp only [shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
      Iso.refl_hom, id_comp, Linear.units_smul_comp, shiftFunctor_obj_d',
      Linear.comp_units_smul, smul_add, smul_smul]

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q +
      (m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow)) •
        K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯ =
    (a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow) • γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q +
      (a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow)) •
        K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯
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π₁ ≫ whiskerRight iso₁.inv (shiftFunctor C 1) = iso₃.inv ≫ A.whiskerLeft π₃Toπ₁

Tactic:
simp only [← cancel_epi iso₃.hom, ← reassoc_of% comm₃, Iso.hom_inv_id_assoc,
        ← whiskerRight_comp, Iso.hom_inv_id, whiskerRight_id']
      apply comp_id

Goal state after:
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
T : Triangle C
H : T ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0

Tactic:
by
  have H₂ := rot_of_distTriang T.rotate (rot_of_distTriang T H)
  simpa using comp_distTriang_mor_zero₁₂ T.rotate.rotate H₂

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 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 =
      (((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

Tactic:
intros

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 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 =
    (((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✝
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
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
⊢ fst ≫ T.mor₁ + T.mor₂ ≫ section_ T.mor₂ = 𝟙 T.obj₂

Tactic:
by simp only [← hfst, sub_add_cancel]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k :
  { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i, g := opcyclesMap S.g i,
        zero := ⋯ }.X₂ ⟶
    A
hk :
  { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i, g := opcyclesMap S.g i,
          zero := ⋯ }.f ≫
      k =
    0
⊢ { l //
    { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i,
            g := opcyclesMap S.g i, zero := ⋯ }.g ≫
        l =
      k }

Tactic:
by
    dsimp at k hk ⊢
    have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_zero])
    dsimp at H
    refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
    · rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ : W.FunctorsInverting D
τ : X✝ ⟶ Y✝
⊢ W.Q ⋙ lift X✝.obj ⋯ = X✝.obj

Tactic:
fac

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ : W.FunctorsInverting D
τ : X✝ ⟶ Y✝
⊢ X✝.obj = X✝.obj
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ : W.FunctorsInverting D
τ : X✝ ⟶ Y✝
⊢ Y✝.obj = W.Q ⋙ lift Y✝.obj ⋯

Tactic:
fac

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ : W.FunctorsInverting D
τ : X✝ ⟶ Y✝
⊢ Y✝.obj = Y✝.obj
Module: Mathlib.CategoryTheory.Localization.Equivalence

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
⊢ L₂.IsLocalization W₂

Tactic:
have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf => by
    obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
    exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (W₂.Q.mapArrow.mapIso e)).1 (Localization.inverts W₂.Q W₂ _ hf')
  exact
    { inverts := hW₂
      isEquivalence :=
        Localization.isEquivalence W₂.Q W₂ L₁ W₁ L₂ (Construction.lift L₂ hW₂)
          (E.functor ⋙ W₂.Q) (Localization.lift (E.functor ⋙ W₂.Q) h L₁) (by
            calc
              L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
              _ ≅ _ := isoWhiskerRight E.counitIso.symm _
              _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    Functor.associator _ _ _
              _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                    isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫
                      isoWhiskerRight iso _)
              _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q :=
                    isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁)
              _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
              _ ≅ 𝟭 C₂ ⋙ W₂.Q := isoWhiskerRight E.counitIso _
              _ ≅ W₂.Q := leftUnitor _)
          (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Lifting.iso W₂.Q W₂ _ _) ≪≫ iso) }

Goal state after: