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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
e : T₁.invRotate ≅ T₂.invRotate := h.choose
h₁ : e.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
h₂ : Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom = e.hom.hom₂
h₃ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃
h₄ :
  (𝟭 C).map e₃.hom ≫ (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₂.obj₃ =
    (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₁.obj₃ ≫
      (shiftFunctor C (-1) ⋙ shiftFunctor C 1).map e₃.hom
⊢ T₁ ≅ T₂

Tactic:
dsimp at h₁ h₂ h₃ h₄

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
e : T₁.invRotate ≅ T₂.invRotate := h.choose
h₁ : e.hom.hom₁ = (shiftFunctor C (-1)).map e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T₁.3) ≫ (shiftFunctor C 1).map e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T₂.3
h₄ :
  e₃.hom ≫ (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₂.obj₃ =
    (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₁.obj₃ ≫
      (shiftFunctor C 1).map ((shiftFunctor C (-1)).map e₃.hom)
⊢ T₁ ≅ T₂
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case nil
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ (of V).obj u) (q : u ⟶ v), P p → P (p ≫ (of V).map q)
b✝ : Paths V
⊢ P Quiver.Path.nil

Tactic:
exact id

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case zero.nil
V : Type u₁
inst✝ : Quiver V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : (of V).obj v ⟶ b) (q : u ⟶ v), P p → P ((of V).map q ≫ p)
h : Quiver.Path.nil.length = 0
⊢ P Quiver.Path.nil

Tactic:
exact id

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 m₃ = w₂₃

Tactic:
dsimp [m₃]

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₁₃ ≫
      (shiftFunctor C 1).map
        ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₃ ≫
          (shiftFunctor C (-1)).map o.m₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₂₃) =
    w₂₃
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₂₃
⊢ m₃ ≫
      (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:
dsimp [m₃]

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.Localization.CalculusOfFractions.ComposableArrows

Goal state before:
pp: case zero
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
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
Y : D
⊢ (L.mapComposableArrows 0).essImage (mk₀ Y)

Tactic:
exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩

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

Goal state before:
pp: case isSuccLimit
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : Order.IsSuccLimit b
hb' : ∀ b_1 < b, P.strictLimitsClosureIter J b_1 ≤ P.limitsClosure J
c : β
⊢ c < b → transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) c P ≤ P.limitsClosure J

Tactic:
hc

Goal state after:
case isSuccLimit
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : Order.IsSuccLimit b
hb' : ∀ b_1 < b, P.strictLimitsClosureIter J b_1 ≤ P.limitsClosure J
c : β
hc : c < b
⊢ transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) c P ≤ P.limitsClosure J
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case isSuccLimit
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b, ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b_1)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b_1)
hb₀ : Small.{w, w'} ↑(Set.Iio b)
⊢ ObjectProperty.Small.{w, v, u} (⨆ x, transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑x) P)

Tactic:
have (c : Set.Iio b) : ObjectProperty.Small.{w}
      (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) c.1 P) := by
      have := H c.2.le
      exact hb' c.1 c.2

Goal state after:
case isSuccLimit
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : Order.IsSuccLimit b
hb' :
  ∀ b_1 < b, ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b_1)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b_1)
hb₀ : Small.{w, w'} ↑(Set.Iio b)
this :
  ∀ (c : ↑(Set.Iio b)), ObjectProperty.Small.{w, v, u} (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑c) P)
⊢ ObjectProperty.Small.{w, v, u} (⨆ x, transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (↑x) P)
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : C
hX : P X
⊢ P.shiftClosure A X

Tactic:
exact ⟨X, 0, (shiftFunctorZero C A).symm.app X, hX⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
⊢ P.limitsOfShape (Discrete PEmpty.{1}) ≤ P

Tactic:
by
    rintro X ⟨p⟩
    obtain ⟨Z, hZ, hZ₂⟩ := P.exists_prop_of_containsZero
    have hX : IsTerminal X :=
      (IsLimit.equivOfNatIsoOfIso p.diag.uniqueFromEmpty _ _
        (by exact Cone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩))).1 p.isLimit
    exact P.prop_of_isZero (IsZero.of_iso hZ
      (IsLimit.conePointUniqueUpToIso hX (IsZero.isTerminal hZ)))

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
⊢ { X₁ := (F.shift n₀).obj T.obj₁, X₂ := (F.shift n₀).obj T.obj₂, X₃ := (F.shift n₀).obj T.obj₃,
      f := (F.shift n₀).map T.mor₁, g := (F.shift n₀).map T.mor₂, zero := ⋯ }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (F.map_distinguished_exact _
    (Triangle.shift_distinguished _ hT n₀))
  exact ShortComplex.isoMk ((F.isoShift n₀).app _)
    (n₀.negOnePow • ((F.isoShift n₀).app _)) ((F.isoShift n₀).app _)
    (by simp) (by simp)

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

Goal state before:
pp: case refine_2
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
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ (L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
        inv (L.mapTriangle.map ψ)).hom₂ =
    b

Tactic:
rw [← cancel_mono (L.mapTriangle.map ψ).hom₂, ← comp_hom₂, assoc, IsIso.inv_hom_id, comp_id]
    dsimp [ψ]
    simp only [Functor.map_comp, reassoc_of% hγ,
      MorphismProperty.LeftFraction.map_comp_map_s_assoc]

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
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P Q R : ObjectProperty C
inst✝¹ : P.IsStableUnderShift ℤ
inst✝ : Q.IsStableUnderShift ℤ
a : ℤ
⊢ P.extensionProduct Q ≤ (P.extensionProduct Q).shift a

Tactic:
intro X ⟨Y, Z, f, g, h, hT, hP, hQ⟩

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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P Q R : ObjectProperty C
inst✝¹ : P.IsStableUnderShift ℤ
inst✝ : Q.IsStableUnderShift ℤ
a : ℤ
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ (P.extensionProduct Q).shift a X
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
T₁ T₃ : Triangle C
mem₁ : T₁ ∈ distinguishedTriangles
mem₃ : T₃ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₃.obj₁
b : T₁.obj₂ ⟶ T₃.obj₂
Z₅ : C
g₅ : T₃.obj₁ ⟶ Z₅
h₅ : Z₅ ⟶ (shiftFunctor C 1).obj T₁.obj₁
mem₅ : Triangle.mk a g₅ h₅ ∈ distinguishedTriangles
mem₅' : P Z₅
Z₄ : C
g₄ : T₃.obj₂ ⟶ Z₄
h₄ : Z₄ ⟶ (shiftFunctor C 1).obj T₁.obj₂
mem₄ : Triangle.mk b g₄ h₄ ∈ distinguishedTriangles
mem₄' : P Z₄
comm : T₁.mor₁ ≫ b = a ≫ T₃.mor₁
Z₂ : C
g₂ : T₃.obj₂ ⟶ Z₂
h₂ : Z₂ ⟶ (shiftFunctor C 1).obj T₁.obj₁
mem₂ : Triangle.mk (T₁.mor₁ ≫ b) g₂ h₂ ∈ distinguishedTriangles
H : Octahedron ⋯ mem₁ mem₄ mem₂
H' : Octahedron ⋯ mem₅ mem₃ mem₂
φ : T₁ ⟶ T₃ := H.triangleMorphism₁ ≫ H'.triangleMorphism₂
⊢ T₁.mor₂ ≫ φ.hom₃ = b ≫ T₃.mor₂

Tactic:
by simpa [φ] using φ.comm₂

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ (homologyFunctor C 0).shiftMap
      ((quotientCompQhIso C).inv.app K ≫
        (ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)).comp
          (ShiftedHom.mk₀ 0 ⋯ ((quotientCompQhIso C).hom.app L)) ⋯)
      a a' h =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L

Tactic:
ShiftedHom.comp_mk₀,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ (homologyFunctor C 0).shiftMap
      ((quotientCompQhIso C).inv.app K ≫
        ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) ≫
          (shiftFunctor (DerivedCategory C) n).map ((quotientCompQhIso C).hom.app L))
      a a' h =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ ((homologyFunctor C 0).shift a).map ((quotientCompQhIso C).inv.app K) ≫
      (homologyFunctor C 0).shiftMap
        (ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) ≫
          (shiftFunctor (DerivedCategory C) n).map ((quotientCompQhIso C).hom.app L))
        a a' h =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L

Tactic:
Functor.shiftMap_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
n : ℤ
f : K ⟶ (shiftFunctor (CochainComplex C ℤ) n).obj L
a a' : ℤ
h : n + a = a'
⊢ ((homologyFunctor C 0).shift a).map ((quotientCompQhIso C).inv.app K) ≫
      (homologyFunctor C 0).shiftMap (ShiftedHom.map f (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)) a a' h ≫
        ((homologyFunctor C 0).shift a').map ((quotientCompQhIso C).hom.app L) =
    (homologyFunctorFactors C a).hom.app K ≫
      (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h ≫
        (homologyFunctorFactors C a').inv.app L
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g ≫ image.ι g = 0 ≫ image.ι g

Tactic:
image.fac,

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ g = 0 ≫ image.ι g
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g ≫ image.ι g = 0 ≫ image.ι g

Tactic:
image.fac,

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ g = 0 ≫ image.ι g
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : 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' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    ((K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv) ≫ extend.mapX φ (e.r j')

Tactic:
extend.mapX_some φ (e.r_eq_some hj)

Goal state after:
case pos
ι : 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' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    ((K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv) ≫
      (extend.XIso K ⋯).hom ≫ φ.f j ≫ (extend.XIso L ⋯).inv