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

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✝¹¹ : HasShift C ℤ
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasZeroObject D
inst✝⁷ : Preadditive C
inst✝⁶ : Preadditive D
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
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₁₃
F : C ⥤ D
inst✝¹ : F.CommShift ℤ
inst✝ : F.IsTriangulated
⊢ F.map (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂ ≫ F.map h.m₃ = F.map (Triangle.mk u₂₃ v₂₃ w₂₃).mor₂

Tactic:
simpa using F.congr_map h.comm₃

Goal state after:
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
a : M
X : C
⊢ (F.shiftIso 0 a a ⋯).hom.app X = (F.shift a).map ((shiftFunctorZero C M).hom.app X)

Tactic:
by
  simp [F.shiftIso_zero a]

Goal state after:
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
a : M
X : C
⊢ (F.shiftIso 0 a a ⋯).inv.app X = (F.shift a).map ((shiftFunctorZero C M).inv.app X)

Tactic:
by
  simp [F.shiftIso_zero a]

Goal state after:
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 Z : C
n : M
f : X ⟶ (shiftFunctor C n).obj Y
g : Y ⟶ Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ (shiftFunctor C n).map g) a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g

Tactic:
by
  simp [shiftMap]

Goal state after:
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 Z : C
n : M
f : X ⟶ Y
g : Y ⟶ (shiftFunctor C n).obj Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ g) a a' ha' = (F.shift a).map f ≫ F.shiftMap g a a' ha'

Tactic:
by
  simp [shiftMap]

Goal state after:
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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms A
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (n : M), (shiftFunctor C n).PreservesZeroMorphisms
X Y : C
n a a' : M
ha' : n + a = a'
⊢ F.shiftMap 0 a a' ha' = 0

Tactic:
by
  simp [shiftMap]

Goal state after:
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 }
⊢ k ≫ S.X₂.iCycles i ≫ S.X₂.d i (c.next i) = 0

Tactic:
iCycles_d,

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 }
⊢ k ≫ 0 = 0
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_2.inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw : W w
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw⟩)) ≫ eqToHom ⋯

Tactic:
have hw : W.Q.map w = (wIso w hw).hom := rfl

Goal state after:
case refine_2.inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)

Tactic:
hInv_iso_hom_app

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫
        B.symm.inverse.map ((iso T.symm.functor R L B.symm.functor).inv.app (T.symm.inverse.obj X)) ≫
          B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫
      (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ (iso T.functor L R B.functor).hom.app ((T.functor ⋙ T.inverse).obj X)
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso (L₁.map f)

Tactic:
by
    rw [← isIso_iff_of_reflects_iso  _ F]
    exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso iso f)).1 (Localization.inverts L₂ W₂ _ (Φ.map _ hf))

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

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
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ z₃.f ≫ { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }.s =
    { Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.s ≫
      { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }.f

Tactic:
by dsimp; rw [assoc, reassoc_of% fac₂₃, fac]

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

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
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ φ₁.map L₂ ⋯ = φ₂.map L₂ ⋯

Tactic:
apply (Localization.uniq L₂ L₁ W).functor.map_injective

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
W : MorphismProperty C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
h : φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map L₂ ⋯) = (Localization.uniq L₂ L₁ W).functor.map (φ₂.map L₂ ⋯)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
h : W.HasLeftCalculusOfFractions
X Y Y' : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.op s
eq : f₁ ≫ s = f₂ ≫ s
⊢ ∃ X' t, ∃ (_ : W.op t), t ≫ f₁ = t ≫ f₂

Tactic:
by
    obtain ⟨X', t, ht, fac⟩ := h.ext f₁.unop f₂.unop s.unop hs (Quiver.Hom.op_inj eq)
    exact ⟨Opposite.op X', t.op, ht, Quiver.Hom.unop_inj fac⟩

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

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✝
W : MorphismProperty Cᵒᵖ
h : W.HasLeftCalculusOfFractions
X Y : C
φ : W.unop.LeftFraction X Y
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s

Tactic:
obtain ⟨ψ, eq⟩ := h.exists_leftFraction φ.op
    exact ⟨ψ.unop, Quiver.Hom.op_inj eq⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ (shiftFunctor C 1).obj X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h : Triangle.mk a b c ∈ distinguishedTriangles
⊢ ∃ Y, ∃ (_ : P Y), ∃ a b, Triangle.mk a b c ∈ distinguishedTriangles

Tactic:
obtain ⟨Y', hY', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ h hX hZ

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ (shiftFunctor C 1).obj X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h : Triangle.mk a b c ∈ distinguishedTriangles
Y' : C
hY' : P Y'
e : (Triangle.mk a b c).obj₂ ≅ Y'
⊢ ∃ Y, ∃ (_ : P Y), ∃ a b, Triangle.mk a b c ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

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
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y

Tactic:
rw [← NatTrans.naturality_assoc]

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (L ⋙ F' a).map f ≫ (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.retracts

Tactic:
intro X Y f hf
  exact ⟨_, _, f, { i := 𝟙 _, r := 𝟙 _}, hf⟩

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

Goal state before:
pp: case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt f i → ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

pp: case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f) → QuasiIsoAt f i

Tactic:
· intro h
    exact h.quasiIso

Goal state after:
case mpr
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f) → QuasiIsoAt f i
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case a
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
⊢ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure ≤ (P.extensionProduct Q).retractClosure

Tactic:
rw [retractClosure_le_iff]
    exact extensionProduct_retractClosure_retractClosure_le P Q

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }
this : Φ.IsLocalizedEquivalence
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence
⊢ (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂

Tactic:
by
    calc
      _ ≅ L₁ ⋙ E₂.functor ⋙ W₂'.Q ⋙ E₃.inverse :=
          Functor.associator _ _ _ ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm _ ≪≫
            Functor.associator _ _ _
      _ ≅ L₁ ⋙ L₂ ⋙ E₃.functor ⋙ E₃.inverse :=
          isoWhiskerLeft _ ((Functor.associator _ _ _).symm ≪≫
            isoWhiskerRight (Φ.catCommSq L₂ W₂'.Q).iso E₃.inverse ≪≫ Functor.associator _ _ _)
      _ ≅ L₁ ⋙ L₂ := isoWhiskerLeft _ (isoWhiskerLeft _ E₃.unitIso.symm ≪≫ L₂.rightUnitor)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (quasiIso C (ComplexShape.up ℤ)).IsCompatibleWithShift ℤ

Tactic:
rw [quasiIso_eq_trW_subcategoryAcyclic]
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ P.trW g ↔ ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

Tactic:
P.trW_iff

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1) ↔
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ P.trW f

Tactic:
refine ⟨Z', g ≫ e.hom, e.inv ≫ h, isomorphic_distinguished _ mem _ ?_, hZ'⟩

Goal state after:
case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
Z' : C
hZ' : P Z'
e : Z ≅ Z'
⊢ Triangle.mk f (g ≫ e.hom) (e.inv ≫ h) ≅ Triangle.mk f g h
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
⊢ P (F.obj Z) ↔ P.trW (F.map s)

Tactic:
eq₂

Goal state after:
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
⊢ P (F.obj Z) ↔ P (F.obj Z)
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯ =
    (single C (ComplexShape.up ℤ) a'').isoWhiskerLeft (shiftFunctorAdd (CochainComplex C ℤ) m n) ≪≫
      ((single C (ComplexShape.up ℤ) a'').associator (CategoryTheory.shiftFunctor (CochainComplex C ℤ) m)
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n)).symm ≪≫
        Functor.isoWhiskerRight (NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯)
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) ≪≫
          NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯

Tactic:
by
    ext
    dsimp
    simp only [shiftFunctorAdd_eq, shiftFunctorAdd'_hom_app_f, XIsoOfEq,
      eqToIso.hom, eqToHom_trans, id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
p : ℤ
⊢ (((inl f).v (p + 1) p ⋯ ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯) ≫ (↑(fst g)).v p (p + 1) ⋯ =
        ((inl f).v (p + 1) p ⋯ ≫
            (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
              p p ⋯) ≫
          (↑(fst g)).v p (p + 1) ⋯ ∧
      ((inl f).v (p + 1) p ⋯ ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯) ≫ (snd g).v p p ⋯ =
        ((inl f).v (p + 1) p ⋯ ≫
            (Cochain.ofHom
                  ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
              p p ⋯) ≫
          (snd g).v p p ⋯) ∧
    (inr f).f p ≫ (δ (-1) 0 ((snd f).comp (inl g) ⋯)).v p p ⋯ =
      (inr f).f p ≫
        (Cochain.ofHom
              ((mappingConeCompTriangle f g).mor₁ ≫ desc (f ≫ g) ((Cochain.ofHom f).comp (inl g) ⋯) (inr g) ⋯)).v
          p p ⋯

Tactic:
simp [map, δ_zero_cochain_comp,
        Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p (by lia) (by lia)]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (map (f ≫ g) g f (𝟙 X₃) ⋯) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (map f (f ≫ g) (𝟙 X₁) g ⋯)) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).inv

Tactic:
rw [← Functor.map_comp, ← Functor.map_comp, ← Functor.map_comp,
    mappingConeCompHomotopyEquiv_hom_inv_id, comp_id,
    mappingConeCompHomotopyEquiv_comm₁ f g,
    mappingConeCompTriangle_mor₂]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
hk' : e.r k' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
rw [extend.d_none_eq_zero' K _ _ hk', comp_zero]

Goal state after: