awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₁.3) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯)) T₂.3
h₄ :
  Eq (α :=
    T₁.obj₃ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1)
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₂.obj₃))
    (e₃.hom ≫ NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₂.obj₃)
    (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_2)) T₁.obj₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom))
⊢ T₁.mor₂ ≫ e₃.hom = Iso.hom (Functor.mapIso Triangle.π₃ e) ≫ T₂.mor₂

Tactic:
simp [← cancel_mono ((shiftFunctorCompIsoId C (-1) 1 (neg_add_cancel 1)).inv.app T₂.obj₃),
      ← h₃, assoc, h₁, h₄]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pretriangulated.Triangle.obj₃, CategoryTheory.cancel_mono, neg_add_cancel, CategoryTheory.shiftFunctorCompIsoId, OfNat.ofNat, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
dsimp :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X_1.obj₁ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y.obj₂)
    ((-Functor.map (shiftFunctor C (A := ℤ) 1) X_1.mor₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₂)
    (Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁ ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) Y.mor₁))
⊢ X_1.rotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₂ =
    Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁ ≫ Y.rotate.mor₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X_1.obj₁ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y.obj₂)
    ((-Functor.map (shiftFunctor C (A := ℤ) 1) X_1.mor₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₂)
    (Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁ ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) Y.mor₁))

Tactic:
simp only [comp_neg, neg_comp, ← Functor.map_comp, f.comm₁]

Premises used: CategoryTheory.Preadditive.comp_neg, CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
dsimp :
  Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) f.hom₃ ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) Y.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
⊢ X_1.invRotate.mor₁ ≫ f.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) f.hom₃ ≫ Y.invRotate.mor₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
simp :
  Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (-Functor.map (shiftFunctor C (A := ℤ) (-1)) (X_1.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) f.hom₃ ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) Y.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)

Tactic:
simp only [comp_neg, ← Functor.map_comp_assoc, ← f.comm₃]

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
rw :
  Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (-(Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (-Functor.map (shiftFunctor C (A := ℤ) (-1)) (X_1.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)

Tactic:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
X_1 Y : Triangle.{v, u} C
f : X_1 ⟶ Y
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) X_1.obj₁) ≫
        f.hom₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)
    (-(Functor.map (shiftFunctor C (A := ℤ) (-1)) X_1.mor₃ ≫
            Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) f.hom₁)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) Y.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) X_1.obj₃ ⟶ Y.obj₁)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
⊢ Functor.IsEquivalence (C := Triangle.{v, u} C) (Equivalence.functor (triangleRotation C))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Rotate
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
X : C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
⊢ Functor.IsEquivalence (C := Triangle.{v, u} C) (Equivalence.inverse (triangleRotation C))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
D : ComposableArrows.{v_2, u_2} ι 2
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _) (X.ω₂.obj D)

Tactic:
X.distinguished' D

Premises used: Set.Mem, CategoryTheory.Triangulated.SpectralObject.distinguished', CategoryTheory.Pretriangulated.Triangle.mk
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _)
    (X.triangle f g)

Tactic:
X.ω₂_obj_distinguished (mk₂ f g)

Premises used: CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished, CategoryTheory.Triangulated.SpectralObject.δ, CategoryTheory.ComposableArrows.Mk₁.obj, Set.Mem, CategoryTheory.Triangulated.SpectralObject.triangle, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.mk₂, CategoryTheory.ComposableArrows.twoδ₂Toδ₁, CategoryTheory.ComposableArrows.homMk₁, CategoryTheory.ComposableArrows.homMk, CategoryTheory.ComposableArrows.Mk₁.map, CategoryTheory.ComposableArrows.Precomp.map, CategoryTheory.ComposableArrows.twoδ₁Toδ₀, CategoryTheory.Pretriangulated.Triangle.mk, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
⊢ Eq (α :=
    (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).obj (Functor.obj (F.mapComposableArrows 2) D₁) ⟶
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).obj
        (Functor.obj (F.mapComposableArrows 2) D₂))
    ((functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).map (Functor.map (F.mapComposableArrows 2) f) ≫
      X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
    (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).map
        (Functor.map (F.mapComposableArrows 2) f))

Tactic:
have := X.δ'.naturality ((F.mapComposableArrows 2).map f)
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
this :
  Eq (α :=
    (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).obj (Functor.obj (F.mapComposableArrows 2) D₁) ⟶
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).obj
        (Functor.obj (F.mapComposableArrows 2) D₂))
    ((functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).map (Functor.map (F.mapComposableArrows 2) f) ≫
      X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
    (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).map
        (Functor.map (F.mapComposableArrows 2) f))
⊢ Eq (α :=
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
      (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).obj
        (Functor.obj (F.mapComposableArrows 2) D₂))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      (functorArrows ι 1 2 2 _proof_2 _proof_4 ⋙ X.ω₁).map (Functor.map (F.mapComposableArrows 2) f) ≫
        X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁) ≫
        (functorArrows ι 0 1 2 _proof_6 _proof_2 ⋙ X.ω₁ ⋙ shiftFunctor C (A := ℤ) 1).map
          (Functor.map (F.mapComposableArrows 2) f))

Tactic:
rw [← cancel_epi (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso _).hom)] at this

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Triangulated.SpectralObject.ω₁
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
D₁ D₂ : ComposableArrows.{u_5, u_4} ι' 2
f : D₁ ⟶ D₂
this :
  Eq (α :=
    X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (CategoryStruct.comp (Y := X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯)))))
        (X.ω₁.map
          ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯))
        (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₂)) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₁.map (homOfLE ⋯))))))
          (X.δ'.app (Functor.obj (F.mapComposableArrows 2) D₁))
          (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))) :
      X.ω₁.obj (Functor.obj (F.mapComposableArrows 1) (mk₁ (D₁.map (homOfLE ⋯)))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
h :
  (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
      Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
        (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom =
    homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₁.map (homOfLE ⋯))))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ (F.map (D₂.map (homOfLE ⋯))))))
    (Functor.map (shiftFunctor C (A := ℤ) 1)
      (X.ω₁.map
        ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
          Functor.map (F.mapComposableArrows 1) (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
            (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom)))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯)))

Tactic:
congr 2
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D_1 : Type u_3
inst_7 : Category.{v_3, u_3} D_1
inst_8 : HasZeroObject.{v_3, u_3} D_1
inst_9 : HasShift.{v_3, u_3, 0} D_1 ℤ
inst_10 : Preadditive.{v_3, u_3} D_1
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D_1 n)
inst_12 : Pretriangulated.{v_3, u_3} D_1
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
D : ComposableArrows.{u_5, u_4} ι' 2
obtain :
  ∀ (w w_1 w_2 : ι') (f : w ⟶ w_1) (g : w_1 ⟶ w_2),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _)
      (Triangle.mk
        ((F.mapComposableArrows 1 ⋙ X.ω₁).map
          (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
        ((F.mapComposableArrows 1 ⋙ X.ω₁).map
          (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
        (NatTrans.app
          {
            app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
              X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
                X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                  Functor.map (shiftFunctor C (A := ℤ) 1)
                    (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
            naturality := ⋯ }
          (mk₂ f g)))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _)
    (Triangle.mk
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) D))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) D))
      (NatTrans.app
        {
          app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
            X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
              X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                Functor.map (shiftFunctor C (A := ℤ) 1)
                  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
          naturality := ⋯ }
        D))

Tactic:
obtain ⟨_, _, _, f, g, rfl⟩ := ComposableArrows.mk₂_surjective D

Premises used: rfl, CategoryTheory.ComposableArrows.mk₂_surjective
-- Module: Mathlib.CategoryTheory.Triangulated.SpectralObject
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
X : SpectralObject.{v_1, u_1, v_2, u_2} C ι
ι' : Type u_4
inst_13 : Category.{u_5, u_4} ι'
F : Functor.{u_5, v_2, u_4, u_2} ι' ι
w w_1 w_2 : ι'
f : w ⟶ w_1
g : w_1 ⟶ w_2
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _)
    (Triangle.mk
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 1 0 2 2 _proof_6 _proof_8 _proof_10 _proof_2 _proof_4) (mk₂ f g)))
      ((F.mapComposableArrows 1 ⋙ X.ω₁).map
        (NatTrans.app (mapFunctorArrows ι' 0 2 1 2 2 _proof_8 _proof_2 _proof_6 _proof_4 _proof_4) (mk₂ f g)))
      (NatTrans.app
        {
          app := fun (D : ComposableArrows.{u_5, u_4} ι' 2) ↦
            X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map' 1 2 _proof_2 _proof_4)).hom ≫
              X.δ'.app (Functor.obj (F.mapComposableArrows 2) D) ≫
                Functor.map (shiftFunctor C (A := ℤ) 1)
                  (X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D.map (homOfLE ⋯))).inv),
          naturality := ⋯ }
        (mk₂ f g)))

Tactic:
isomorphic_distinguished _ (X.triangle_distinguished (F.map f) (F.map g)) _ ?_

Premises used: CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Triangulated.SpectralObject.triangle_distinguished