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

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

Tactic:
assoc,

Goal state after:
case refine_1
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₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₂ ≫
      (shiftFunctor C (-1)).map o.m₁ ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₁₃ ≫
          (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
            (shiftFunctor C (-1)).map ((shiftFunctor C 1).map v₁₃) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₁ =
    v₁₂
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') ≫ φ.map p =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g' ≫ φ.map p

Tactic:
ih,

Goal state after:
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
⊢ (Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
        Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g') ≫
      φ.map p =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g' ≫ φ.map p
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case refine_1
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 : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
H : { l // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ S.X₂.d (c.prev i) i ≫ S.X₂.pOpcycles i ≫ k = 0

Tactic:
d_pOpcycles_assoc,

Goal state after:
case refine_1
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 : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
H : { l // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ 0 ≫ k = 0
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
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''
⊢ (F.shiftIso n a a' ha').hom.app X ≫ F.shiftMap f a' a'' ha'' =
    (F.shift a).map ((shiftFunctor C n).map f) ≫
      (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app Y) ≫ (F.shiftIso mn a a'' ⋯).hom.app Y

Tactic:
simp only [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'' Y,
    ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
    id_comp, comp_obj, shiftIso_hom_naturality_assoc, shiftMap]

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✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0

Tactic:
assoc,

Goal state after:
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✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ k ≫ S.X₂.iCycles i ≫ S.g.f i = 0
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y b✝ c✝ : Paths V
g : Quiver.Path X b✝
e : b✝ ⟶ c✝
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ F.map g ≫ F.map e.toPath = eqToHom ⋯ ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom ⋯

Tactic:
ih,

Goal state after:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y b✝ c✝ : Paths V
g : Quiver.Path X b✝
e : b✝ ⟶ c✝
ih : F.map g = eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯
⊢ (eqToHom ⋯ ≫ G.map g ≫ eqToHom ⋯) ≫ F.map e.toPath = eqToHom ⋯ ≫ (G.map g ≫ G.map e.toPath) ≫ eqToHom ⋯
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case refine_1
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✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ (↑H ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i) = 0 ≫ S.f.f (c.next i)

Tactic:
assoc,

Goal state after:
case refine_1
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✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
H : { l // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
⊢ ↑H ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i) = 0 ≫ S.f.f (c.next i)
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.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
this : Mono S.f
⊢ (x₁ ≫ S.X₁.d j k) ≫ S.f.f k = 0 ≫ S.f.f k

Tactic:
assoc,

Goal state after:
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.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
this : Mono S.f
⊢ x₁ ≫ S.X₁.d j k ≫ S.f.f k = 0 ≫ S.f.f k
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

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

Tactic:
assoc,

Goal state after:
case refine_4
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₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
      ((shiftFunctor C (-1)).map o.m₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₂₃) ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₂₃ ≫
          (shiftFunctor C (-1)).map ((shiftFunctor C 1).map v₂₃) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₂ =
    v₁₃ ≫ u₁₂
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

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

Tactic:
assoc,

Goal state after:
case refine_4
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₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
      (shiftFunctor C (-1)).map o.m₃ ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₂₃ ≫
          (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₂₃ ≫
            (shiftFunctor C (-1)).map ((shiftFunctor C 1).map v₂₃) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₂ =
    v₁₃ ≫ u₁₂
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.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.f.f j = ((x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j) ≫ S.X₂.iCycles j

Tactic:
assoc,

Goal state after:
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.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.f.f j = (x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j ≫ S.X₂.iCycles j
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.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.f.f j = (x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j ≫ S.X₂.iCycles j

Tactic:
assoc,

Goal state after:
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.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.f.f j = x₂ ≫ S.X₂.pOpcycles i ≫ S.X₂.opcyclesToCycles i j ≫ S.X₂.iCycles j
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
L✝ : C ⥤ D
W✝ : MorphismProperty C
E✝ : Type u_3
inst✝³ : Category.{v_3, u_3} E✝
inst✝² : L✝.IsLocalization W✝
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
E : Type u_4
inst✝ : Category.{v_4, u_4} E
⊢ ((whiskeringLeft C D E).obj L).FullyFaithful

Tactic:
by
  have := full_whiskeringLeft L W E
  have := faithful_whiskeringLeft L W E
  exact FullyFaithful.ofFullyFaithful _

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv ≫ (isoOfHom L W f hf).hom =
    (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X ≫ (isoOfHom L W f hf).hom
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map f ≫ e.hom.app Y = L.map g

Tactic:
← NatIso.naturality_1 e g

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (W.Q ⋙ (Localization.uniq W.Q L W).functor).map g ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map f ≫ e.hom.app Y = W.Q.map g

Tactic:
← NatIso.naturality_1 e g

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map f ≫ e.hom.app Y =
    e.inv.app X ≫ (L ⋙ (Localization.uniq L W.Q W).functor).map g ≫ e.hom.app Y