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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 2 1 = d₁

Tactic:
change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁
  rw [if_pos rfl, Category.id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
⊢ Epi (K.homologyπ i)

Tactic:
dsimp only [homologyπ]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ K.d j i ≫ K.d i i' ≫ x = 0

Tactic:
K.d_comp_d_assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j✝ k✝ : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
⊢ 0 ≫ x = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ K.d j i ≫ K.d i i' ≫ x = 0

Tactic:
K.d_comp_d_assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ 0 ≫ x = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' (c.prev j) j (c.next j)).HasHomology
⊢ (K.homologyIsoSc' (c.prev j) j (c.next j) ⋯ ⋯).hom = (Iso.refl (K.homology j)).hom

Tactic:
apply ShortComplex.homologyMap_id

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inr.f i ≫ biprod.fst.f i = 0

Tactic:
rw [← comp_f, biprod.inr_fst, zero_f]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ D
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.rightOp.map f)

Tactic:
by
  have := h f.op hf
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.unop.map f)

Tactic:
by
  have := h f.op hf
  dsimp
  infer_instance

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

Goal state before:
pp: case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
h✝ : ¬c.Rel j i
⊢ G.map 0 = 0

Tactic:
· rw [G.map_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
⊢ z₁.comp (ofHom (𝟙 G)) ⋯ = z₁

Tactic:
ext p q hpq
  simp only [comp_zero_cochain_v, ofHom_v, HomologicalComplex.id_f, comp_id]

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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
H : (φ ≫ α).f (c.next j) = (dNext (c.next j)) hα.hom + (prevD (c.next j)) hα.hom + Hom.f 0 (c.next j)
⊢ fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) + sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j) =
    d φ j (c.next j) ≫
      if h : c.Rel (c.next j) (c.next (c.next j)) then
        fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j) +
          sndX φ (c.next j) ≫ α.f (c.next j)
      else sndX φ (c.next j) ≫ α.f (c.next j)

Tactic:
simp only [comp_f, zero_f, add_zero, prevD_eq _ hjk] at H

Goal state after:
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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
H : φ.f (c.next j) ≫ α.f (c.next j) = (dNext (c.next j)) hα.hom + hα.hom (c.next j) j ≫ K.d j (c.next j)
⊢ fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j) + sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j) =
    d φ j (c.next j) ≫
      if h : c.Rel (c.next j) (c.next (c.next j)) then
        fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j) +
          sndX φ (c.next j) ≫ α.f (c.next j)
      else sndX φ (c.next j) ≫ α.f (c.next j)
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
A : C
f g : A ⟶ (mappingCone φ).X i
⊢ f ≫ (↑(fst φ)).v i j hij = g ≫ (↑(fst φ)).v i j hij ∧ f ≫ (snd φ).v i i ⋯ = g ≫ (snd φ).v i i ⋯ → f = g

Tactic:
rintro ⟨h₁, h₂⟩

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
A : C
f g : A ⟶ (mappingCone φ).X i
h₁ : f ≫ (↑(fst φ)).v i j hij = g ≫ (↑(fst φ)).v i j hij
h₂ : f ≫ (snd φ).v i i ⋯ = g ≫ (snd φ).v i i ⋯
⊢ f = g
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 : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
⊢ (inl φ).v i j ⋯ ≫ f = (inl φ).v i j ⋯ ≫ g ∧ (inr φ).f j ≫ f = (inr φ).f j ≫ g → f = g

Tactic:
rintro ⟨h₁, h₂⟩

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 : j + 1 = i
A : C
f g : (mappingCone φ).X j ⟶ A
h₁ : (inl φ).v i j ⋯ ≫ f = (inl φ).v i j ⋯ ≫ g
h₂ : (inr φ).f j ≫ f = (inr φ).f j ≫ g
⊢ f = g
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
⊢ γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij ∧ γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯ → γ₁ = γ₂

Tactic:
rintro ⟨h₁, h₂⟩

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
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
⊢ γ₁ = γ₂
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 (mappingCone φ) K j
⊢ (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯ ∧ (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯ →
    γ₁ = γ₂

Tactic:
rintro ⟨h₁, h₂⟩

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 (mappingCone φ) K j
h₁ : (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯
h₂ : (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯
⊢ γ₁ = γ₂
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✝ : X ⟶ Y
f g : X.as ⟶ Y.as
hfg : r f g
⊢ r (-f) (-g)

Tactic:
apply Congruence.equivalence.symm

Goal state after:
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✝ : X ⟶ Y
f g : X.as ⟶ Y.as
hfg : r f g
⊢ r (-g) (-f)
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 ι
W : Type u_3
inst✝³ : Category.{v_1, u_3} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
c : ComplexShape ι
⊢ ∀ ⦃X Y : HomotopyCategory V c⦄ (f : X ⟶ Y),
    (F.mapHomotopyCategory c).map f ≫ (HomotopyCategory.quotient W c).map ((mapHomologicalComplex α c).app Y.as) =
      (HomotopyCategory.quotient W c).map ((mapHomologicalComplex α c).app X.as) ≫ (G.mapHomotopyCategory c).map f

Tactic:
rintro ⟨C⟩ ⟨D⟩ ⟨f : C ⟶ D⟩

Goal state after:
case mk
R : Type u_1
inst✝⁶ : Semiring R
ι : Type u_2
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
W : Type u_3
inst✝³ : Category.{v_1, u_3} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
c : ComplexShape ι
C D : HomologicalComplex V c
f✝ : { as := C } ⟶ { as := D }
f : C ⟶ D
⊢ (F.mapHomotopyCategory c).map (Quot.mk (HomRel.CompClosure (homotopic V c)) f) ≫
      (HomotopyCategory.quotient W c).map ((mapHomologicalComplex α c).app { as := D }.as) =
    (HomotopyCategory.quotient W c).map ((mapHomologicalComplex α c).app { as := C }.as) ≫
      (G.mapHomotopyCategory c).map (Quot.mk (HomRel.CompClosure (homotopic V c)) f)
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
n : A
⊢ s (n + 0) = s n ⋙ 𝟭 D

Tactic:
rw [add_zero]; rfl

Goal state after:
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 G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
a : A
⊢ (commShiftIso F a).hom ≫ whiskerRight e.hom (shiftFunctor D a) =
    (shiftFunctor C a).whiskerLeft e.hom ≫ (commShiftIso G a).hom

Tactic:
by ext; simp [ofIso_commShiftIso_hom_app]

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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C
u₁₂' : X₁' ⟶ X₂'
u₂₃' : X₂' ⟶ X₃'
u₁₃' : X₁' ⟶ X₃'
comm' : u₁₂' ≫ u₂₃' = u₁₃'
e₁ : X₁ ≅ X₁'
e₂ : X₂ ≅ X₂'
e₃ : X₃ ≅ X₃'
comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂'
comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ u₂₃'
v₁₂' : X₂' ⟶ Z₁₂'
w₁₂' : Z₁₂' ⟶ (shiftFunctor C 1).obj X₁'
h₁₂' : Triangle.mk u₁₂' v₁₂' w₁₂' ∈ distinguishedTriangles
v₂₃' : X₃' ⟶ Z₂₃'
w₂₃' : Z₂₃' ⟶ (shiftFunctor C 1).obj X₂'
h₂₃' : Triangle.mk u₂₃' v₂₃' w₂₃' ∈ distinguishedTriangles
v₁₃' : X₃' ⟶ Z₁₃'
w₁₃' : Z₁₃' ⟶ (shiftFunctor C 1).obj X₁'
h₁₃' : Triangle.mk u₁₃' v₁₃' w₁₃' ∈ distinguishedTriangles
H : Octahedron comm' h₁₂' h₂₃' h₁₃'
iso₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ≅ Triangle.mk u₁₂' v₁₂' w₁₂' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂
iso₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ≅ Triangle.mk u₂₃' v₂₃' w₂₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃
iso₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ≅ Triangle.mk u₁₃' v₁₃' w₁₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯
eq₁₂ :
  v₁₂ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ =
    e₂.hom ≫ v₁₂'
eq₁₂' :
  w₁₂ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ ≫ w₁₂'
eq₁₃ :
  v₁₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ =
    e₃.hom ≫ v₁₃'
eq₁₃' :
  w₁₃ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ ≫ w₁₃'
eq₂₃ :
  v₂₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ =
    e₃.hom ≫ v₂₃'
eq₂₃' :
  w₂₃ ≫ (shiftFunctor C 1).map e₂.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ ≫ w₂₃'
rel₁₂ : v₁₂' ≫ H.m₁ = u₂₃' ≫ v₁₃'
rel₁₃ : w₁₂' = H.m₁ ≫ w₁₃'
rel₂₂ : v₁₃' ≫ H.m₃ = v₂₃'
rel₂₃ : w₁₃' ≫ (shiftFunctor C 1).map u₁₂' = H.m₃ ≫ w₂₃'
⊢ (iso₁₂.hom.hom₃ ≫ H.m₁ ≫ iso₁₃.inv.hom₃) ≫ w₁₃ = w₁₂

Tactic:
rw [← cancel_mono (e₁.hom⟦(1 : ℤ)⟧'), eq₁₂', assoc, assoc, assoc, eq₁₃',
      iso₁₃.inv_hom_id_triangle_hom₃_assoc, ← rel₁₃]

Goal state after:
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
inst✝ : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ (shiftFunctor C m).obj Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = a''

Tactic:
rw [← ha'', ← ha', ← hnm, add_assoc]

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 ((shiftFunctor C (-1)).map o.m₁) ≫
          (shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app ((shiftFunctor C 1).obj Z₁₃) =
    u₂₃ ≫ w₁₃

Tactic:
shift_shiftFunctorCompIsoId_inv_app,

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₁₂ ≫
      (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app ((shiftFunctor C 1).obj Z₁₂) ≫
        (shiftFunctor C 1).map ((shiftFunctor C (-1)).map o.m₁) ≫
          (shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app ((shiftFunctor C 1).obj Z₁₃) =
    u₂₃ ≫ w₁₃
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case cons
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Path X Y
b✝ c✝ : C
g : Path Y b✝
e : b✝ ⟶ c✝
ih : composePath (f.comp g) = composePath f ≫ composePath g
⊢ composePath (f.comp (g.cons e)) = composePath f ≫ composePath (g.cons e)

Tactic:
simp [ih]

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

Goal state before:
pp: case refine_3
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 ((shiftFunctor C 1).obj Z₂₃) =
    w₂₃

Tactic:
shift_shiftFunctorCompIsoId_inv_app,

Goal state after:
case refine_3
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₁₃ ≫
      (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app ((shiftFunctor C 1).obj Z₁₃) ≫
        (shiftFunctor C 1).map ((shiftFunctor C (-1)).map o.m₃) ≫
          (shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app ((shiftFunctor C 1).obj Z₂₃) =
    w₂₃
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
this✝ : L.EssSurj
this : AddCommGroup (L.obj (L.objPreimage X') ⟶ L.obj (L.objPreimage Y')) :=
  addCommGroup' L W (L.objPreimage X') (L.objPreimage Y')
⊢ AddCommGroup (X' ⟶ Y')

Tactic:
exact Equiv.addCommGroup (homEquiv (L.objObjPreimageIso X') (L.objObjPreimageIso Y'))

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝¹² : Category.{v_1, u_1} C₁
inst✝¹¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C₁ M
inst✝⁸ : HasShift C₂ M
inst✝⁷ : Φ.functor.CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{v_3, u_4} D₁
inst✝⁵ : Category.{v_4, u_5} D₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : HasShift D₁ M
inst✝² : HasShift D₂ M
inst✝¹ : L₁.CommShift M
inst✝ : L₂.CommShift M
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
m : M
X : C₁
⊢ (Functor.commShiftIso G m).inv.app (L₁.obj X) =
    (shiftFunctor D₂ m).map (e.inv.app X) ≫
      (Functor.commShiftIso L₂ m).inv.app (Φ.functor.obj X) ≫
        L₂.map ((Functor.commShiftIso Φ.functor m).inv.app X) ≫
          e.hom.app ((shiftFunctor C₁ m).obj X) ≫ G.map ((Functor.commShiftIso L₁ m).hom.app X)

Tactic:
simp [Functor.commShiftOfLocalization_iso_inv_app,
    Functor.commShiftIso_comp_inv_app]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure ≤ P.limitsClosure J

Tactic:
rw [isoClosure_le_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P ≤ P.limitsClosure J