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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive 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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₃ :
  ((shiftFunctor C 1).map w₁₃.unop ≫ (shiftFunctor C 1).map o.m₃).op ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁ =
    ((shiftFunctor C 1).map w₁₂.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁
⊢ o.m₃.op ≫ w₁₃ = w₁₂

Tactic:
← Functor.map_comp,

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive 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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₃ :
  ((shiftFunctor C 1).map (w₁₃.unop ≫ o.m₃)).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁ =
    ((shiftFunctor C 1).map w₁₂.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁
⊢ o.m₃.op ≫ w₁₃ = w₁₂
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive 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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map w₂₃.unop ≫ (shiftFunctor C 1).map o.m₁).op ≫
      (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂ =
    (((shiftFunctor C 1).map w₁₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁) ≫ u₁₂
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃

Tactic:
← Functor.map_comp,

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive 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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
eq₂ :
  ((shiftFunctor C 1).map (w₂₃.unop ≫ o.m₁)).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₂ =
    (((shiftFunctor C 1).map w₁₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app X₁) ≫ u₁₂
⊢ w₁₃ ≫ (shiftFunctor Cᵒᵖ 1).map u₁₂ = o.m₁.op ≫ w₂₃
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f s b ∈ Pretriangulated.distinguishedTriangles
⊢ B.trW s

Tactic:
trW_iff'

Goal state after:
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ Z s' b, A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
X Y : C
f : X ⟶ Y
hX : B X
hY : A Y
Z : C
s : Y ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f s b ∈ Pretriangulated.distinguishedTriangles
⊢ ∃ X f h, ∃ (_ : Triangle.mk f s h ∈ Pretriangulated.distinguishedTriangles), B X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

Goal state before:
pp: 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
P : ObjectProperty C
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsGE (((P.tStructure t).truncGE n₁).obj { obj := T.obj₂, property := h₂ }).obj n₁

Tactic:
← P.tStructure_isGE_iff

Goal state after:
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
P : ObjectProperty C
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ (P.tStructure t).IsGE (((P.tStructure t).truncGE n₁).obj { obj := T.obj₂, property := h₂ }) n₁
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : HomotopyCategory.Plus C
x✝ : CochainComplex.IsKInjective L.obj.as
this : Function.Bijective (DerivedCategory.Qh.map ∘ (HomotopyCategory.Plus.ι C).map)
⊢ Function.Bijective Qh.map

Tactic:
← Function.Bijective.of_comp_iff' (t.plus.fullyFaithfulι.map_bijective _ _)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : HomotopyCategory.Plus C
x✝ : CochainComplex.IsKInjective L.obj.as
this : Function.Bijective (DerivedCategory.Qh.map ∘ (HomotopyCategory.Plus.ι C).map)
⊢ Function.Bijective (t.plus.ι.map ∘ Qh.map)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
⊢ ∀ (f : T ⟶ T'), f.hom₂ = 0 → f = 0

Tactic:
intro f

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
⊢ f.hom₂ = 0 → f = 0
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this✝ : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
φ' : (A.ι ⋙ L₂).obj X₁ ⟶ (A.ι ⋙ L₂).obj X₂
hφ' : φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂
f : B.trW.LeftFraction (A.ι.obj X₁) (A.ι.obj X₂)
hf : φ' = f.map L₂ ⋯
X₃ : C
s' : A.ι.obj X₂ ⟶ X₃
a : f.Y' ⟶ X₃
hX₃ : A X₃
hs' : (A ⊓ B).trW s'
fac : f.s ≫ a = s'
g : (B.inverseImage A.ι).trW.LeftFraction X₁ X₂ :=
  { Y' := { obj := X₃, property := hX₃ }, f := homMk (f.f ≫ a), s := homMk s', hs := ⋯ }
this : IsIso (L₁.map g.s)
⊢ F.map (g.map L₁ ⋯) ≫ F.map (L₁.map g.s) = φ ≫ F.map (L₁.map g.s)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
this✝ : L₁.EssSurj
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
φ : F.obj (L₁.obj X₁) ⟶ F.obj (L₁.obj X₂)
φ' : (A.ι ⋙ L₂).obj X₁ ⟶ (A.ι ⋙ L₂).obj X₂
hφ' : φ = e.inv.app X₁ ≫ φ' ≫ e.hom.app X₂
f : B.trW.LeftFraction (A.ι.obj X₁) (A.ι.obj X₂)
hf : φ' = f.map L₂ ⋯
X₃ : C
s' : A.ι.obj X₂ ⟶ X₃
a : f.Y' ⟶ X₃
hX₃ : A X₃
hs' : (A ⊓ B).trW s'
fac : f.s ≫ a = s'
g : (B.inverseImage A.ι).trW.LeftFraction X₁ X₂ :=
  { Y' := { obj := X₃, property := hX₃ }, f := homMk (f.f ≫ a), s := homMk s', hs := ⋯ }
this : IsIso (L₁.map g.s)
⊢ F.map (g.map L₁ ⋯ ≫ L₁.map g.s) = φ ≫ F.map (L₁.map g.s)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst✝ : t.IsGE Y n
⊢ ∀ (f : (t.truncGE n).obj X ⟶ Y), (t.truncGEπ n).app X ≫ f = 0 → f = 0

Tactic:
intro f

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
f₁ f₂ : (t.truncGE n).obj X ⟶ Y
h : (t.truncGEπ n).app X ≫ f₁ = (t.truncGEπ n).app X ≫ f₂
inst✝ : t.IsGE Y n
f : (t.truncGE n).obj X ⟶ Y
⊢ (t.truncGEπ n).app X ≫ f = 0 → f = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
⊢ ∀ (f : Y ⟶ (t.truncLT n).obj X), f ≫ (t.truncLTι n).app X = 0 → f = 0

Tactic:
intro f

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
n : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
f : Y ⟶ (t.truncLT n).obj X
⊢ f ≫ (t.truncLTι n).app X = 0 → f = 0
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk

Tactic:
· simp only [map, Nat.reduceAdd]
            rw [hj (fun n ↦ f (n + 1)) (k + 1) (by lia) (by lia)]
            obtain _ | j := j
            all_goals simp [map]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b : ℤ
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ ((t.truncGE a).map ((t.truncLT b).map x✝) ≫
        t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x✝¹ ≫ (t.truncGEπ a).app x✝¹) a) (b - 1) b ⋯) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x✝¹) =
    (t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x✝² ≫ (t.truncGEπ a).app x✝²) a) (b - 1) b ⋯ ≫
        (t.truncLT b).map ((t.truncGE a).map x✝)) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x✝¹)

Tactic:
exact t.from_truncGE_obj_ext (by simp)

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip✝ : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
hip : QuasiIso i ∨ QuasiIso p
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝¹ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝ : ∀ (n : ℤ), Injective ((kernel p).X n)
this : (kernel p).IsKInjective
⊢ ∃ α, δ 0 1 α = ↑β

Tactic:
cases hip
      · refine IsKInjective.eq_δ_of_cocycle β ?_ 0 (by simp)
        have : (ShortComplex.mk _ _ (cokernel.condition i)).ShortExact :=
          { exact := ShortComplex.exact_cokernel i }
        exact this.acyclic_X₃ (by dsimp; infer_instance)
      · refine IsKInjective.eq_δ_of_cocycle' β ?_ 0 (by simp)
        have := hp.epi
        have : (ShortComplex.mk _ _ (kernel.condition p)).ShortExact :=
          { exact := ShortComplex.exact_kernel p }
        exact this.acyclic_X₁ (by dsimp; infer_instance)

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
⊢ mk f₀ = mk f₁

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject

Goal state after:
case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
f₀ f₁ : Y ⟶ Z
h✝ : RightHomotopyRel (f ≫ f₀) (f ≫ f₁)
P : PathObject Z
left✝ : P.IsGood
h : P.RightHomotopy (f ≫ f₀) (f ≫ f₁)
⊢ mk f₀ = mk f₁
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app X₂)

Tactic:
rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasRightResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app X₂)

Tactic:
rw [← NatTrans.isIso_app_iff_of_iso α ((Φ.functor ⋙ L₂).objObjPreimageIso X₂)]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_4
H : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₂
inst✝² : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
F G : D₂ ⥤ H
α : F ⟶ G
hα : ∀ (X₁ : C₁), IsIso (α.app (L₂.obj (Φ.functor.obj X₁)))
X₂ : D₂
this : (Φ.functor ⋙ L₂).EssSurj
⊢ IsIso (α.app ((Φ.functor ⋙ L₂).obj ((Φ.functor ⋙ L₂).objPreimage X₂)))
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
hi' : ¬i + 1 < n
⊢ Mono
    { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology (i + 1),
        f := ⋯.δ i (i + 1) ⋯,
        g := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.f (i + 1),
        zero := ⋯ }.g

Tactic:
· obtain rfl : n = i + 1 := by lia
      infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE (n + 1)
⊢ ∃ K', ∃ (_ : K'.IsStrictlyGE (n + 1)), ∃ ι π, Mono ι ∧ QuasiIso ι ∧ degreewiseEpiWithInjectiveKernel π ∧ ι ≫ π = f

Tactic:
exact ⟨mid f n, inferInstance, ι f n, π f n, inferInstance,
    inferInstance, degreewiseEpiWithInjectiveKernel_π f n, ι_π f n⟩

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.HorizontalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
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} D₁
inst✝⁴ : Category.{v_5, u_5} D₂
inst✝³ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst✝² : B₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ₕ w').GuitartExact
Y₂ : D₂
⊢ (w'.costructuredArrowRightwards Y₂).Final

Tactic:
costructuredArrowRightwards_final_iff_of_iso _ (B₁.objObjPreimageIso Y₂).symm

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
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} D₁
inst✝⁴ : Category.{v_5, u_5} D₂
inst✝³ : Category.{v_6, u_6} D₃
V₁ : C₁ ⥤ D₁
T₁ : C₁ ⥤ C₂
B₁ : D₁ ⥤ D₂
V₂ : C₂ ⥤ D₂
w : TwoSquare T₁ V₁ V₂ B₁
T₂ : C₂ ⥤ C₃
B₂ : D₂ ⥤ D₃
V₃ : C₃ ⥤ D₃
w' : TwoSquare T₂ V₂ V₃ B₂
inst✝² : B₁.EssSurj
inst✝¹ : w.GuitartExact
inst✝ : (w ≫ₕ w').GuitartExact
Y₂ : D₂
⊢ (w'.costructuredArrowRightwards (B₁.obj (B₁.objPreimage Y₂))).Final
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.descShortComplex S)) ≫
      F.mapDerivedCategory.map (triangleOfSESδ hS) =
    F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.descShortComplex S)) ≫
      F.mapDerivedCategoryFactors.hom.app S.X₃ ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.descShortComplex S) ≫ triangleOfSESδ hS) =
    F.mapDerivedCategory.map (Q.map (CochainComplex.mappingCone.descShortComplex S)) ≫
      F.mapDerivedCategoryFactors.hom.app S.X₃ ≫
        triangleOfSESδ ⋯ ≫
          (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)