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₂
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ :
  (-Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b =
    a ≫ (-Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₁)
⊢ Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b =
    a ≫ Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₁

Tactic:
rw [neg_comp, comp_neg, neg_inj] at ha₂

Premises used: CategoryTheory.Preadditive.comp_neg, neg_inj, CategoryTheory.Preadditive.neg_comp
-- 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₂
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ :
  Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b =
    a ≫ Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₁
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁ ⟶
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₂.obj₂)
    (Functor.map (shiftFunctor C (A := ℤ) 1) (T₁.mor₁ ≫ b))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁))

Tactic:
simpa only [Functor.map_comp, Functor.map_preimage] using ha₂

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.map_preimage
-- 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₂
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃
ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂
ha₂ : T₁.rotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) b = a ≫ T₂.rotate.mor₃
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.preimage (shiftFunctor C (A := ℤ) 1) a) = c ≫ T₂.mor₃

Tactic:
simpa only [Functor.map_preimage] using ha₁

Premises used: CategoryTheory.Functor.map_preimage
-- 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₂
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
dsimp :
  Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁) ≫
        a :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) c ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₂.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
⊢ T₁.invRotate.mor₁ ≫ a = Functor.map (shiftFunctor C (A := ℤ) (-1)) c ≫ T₂.invRotate.mor₁

Tactic:
dsimp
-- 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₂
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁) ≫
        a :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) c ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₂.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)

Tactic:
simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm,
      Functor.map_comp, shift_shift_neg', Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shift_shift_neg', CategoryTheory.Preadditive.comp_neg, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.id_obj, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- 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₂
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
obtain :
  ∀ (a_1 : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃) (ha₁ : T₁.invRotate.mor₂ ≫ a_1 = a ≫ T₂.invRotate.mor₂)
    (ha₂ :
      T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) c) =
        a_1 ≫ T₂.invRotate.mor₃),
    ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂
⊢ ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Tactic:
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
    (inv_rot_of_distTriang _ hT₁) (inv_rot_of_distTriang _ hT₂) (c⟦(-1 : ℤ)⟧') a (by
    dsimp
    simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm,
      Functor.map_comp, shift_shift_neg', Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id])

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, OfNat.ofNat, Neg.neg
-- 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₂
a_1 : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a_1 = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a_1 ≫ T₂.invRotate.mor₂
ha₂ :
  T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) c) =
    a ≫ T₂.invRotate.mor₃
⊢ ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a_1 ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Tactic:
⟨a, ⟨ha₁, ?_⟩⟩

Premises used: And.intro, Exists.intro
-- 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₂
a_1 : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a_1 = c ≫ T₂.mor₃
a : T₁.invRotate.obj₃ ⟶ T₂.invRotate.obj₃
ha₁ : T₁.invRotate.mor₂ ≫ a = a_1 ≫ T₂.invRotate.mor₂
ha₂ :
  T₁.invRotate.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.map (shiftFunctor C (A := ℤ) (-1)) c) =
    a ≫ T₂.invRotate.mor₃
refine : T₁.mor₂ ≫ c = a ≫ T₂.mor₂
⊢ ∃ (b : T₁.obj₂ ⟶ T₂.obj₂), T₁.mor₁ ≫ b = a_1 ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Tactic:
refine ⟨a, ⟨ha₁, ?_⟩⟩
-- 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
X : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (X := 0) 0 (𝟙 X) 0)

Tactic:
isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished X)) _ ?_

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, CategoryTheory.Pretriangulated.contractible_distinguished
-- 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
X : C
refine : Iso (C := Triangle.{v, u} C) (Triangle.mk (X := 0) 0 (𝟙 X) 0) (Triangle.invRotate (contractibleTriangle X))
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (X := 0) 0 (𝟙 X) 0)

Tactic:
refine isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished X)) _ ?_

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, CategoryTheory.Pretriangulated.contractible_distinguished
-- 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
X : C
⊢ Triangle.mor₁ (Triangle.mk (X := 0) 0 (𝟙 X) 0) ≫
      Iso.hom (Iso.refl (Triangle.obj₂.{v, u} (Triangle.mk (X := 0) 0 (𝟙 X) 0))) =
    CategoryStruct.comp (Y := Triangle.obj₁.{v, u} (Triangle.invRotate (contractibleTriangle X)))
      (Iso.hom (Iso.symm (Functor.mapZeroObject (shiftFunctor C (A := ℤ) (-1)))))
      (Triangle.mor₁ (Triangle.invRotate (contractibleTriangle X)))

Tactic:
simp
-- 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
X : C
⊢ Triangle.mor₂ (Triangle.mk (X := 0) 0 (𝟙 X) 0) ≫
      Iso.hom (Iso.refl (Triangle.obj₃.{v, u} (Triangle.mk (X := 0) 0 (𝟙 X) 0))) =
    Iso.hom (Iso.refl (Triangle.obj₂.{v, u} (Triangle.mk (X := 0) 0 (𝟙 X) 0))) ≫
      Triangle.mor₂ (Triangle.invRotate (contractibleTriangle X))

Tactic:
simp
-- 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
X : C
⊢ Triangle.mor₃ (Triangle.mk (X := 0) 0 (𝟙 X) 0) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.symm (Functor.mapZeroObject (shiftFunctor C (A := ℤ) (-1))))) =
    Iso.hom (Iso.refl (Triangle.obj₃.{v, u} (Triangle.mk (X := 0) 0 (𝟙 X) 0))) ≫
      Triangle.mor₃ (Triangle.invRotate (contractibleTriangle X))

Tactic:
simp
-- 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
X : C
⊢ Iso (C := Triangle.{v, u} C) (Triangle.mk (X := 0) 0 (𝟙 X) 0) (Triangle.invRotate (contractibleTriangle X))

Tactic:
exact Triangle.isoMk _ _ (Functor.mapZeroObject _).symm (Iso.refl _) (Iso.refl _)
    (by simp) (by simp) (by simp)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- 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
X : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)))

Tactic:
isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ ?_

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, OfNat.ofNat, CategoryTheory.Pretriangulated.contractible_distinguished₁, CategoryTheory.Functor.obj
-- 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
X : C
refine :
  Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) ≅
    Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)))

Tactic:
refine isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ ?_

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, OfNat.ofNat, CategoryTheory.Pretriangulated.contractible_distinguished₁, CategoryTheory.Functor.obj
-- 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
X : C
⊢ (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).mor₁ ≫
      Iso.hom (Iso.refl (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).obj₂) =
    CategoryStruct.comp (Y :=
      Triangle.obj₁.{v, u}
        (Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)))
      (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X) :
        (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).obj₁ ⟶
          Triangle.obj₁.{v, u}
            (Triangle.invRotate
              (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)))
      (Triangle.mor₁
          (Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)) :
        Triangle.obj₁.{v, u}
            (Triangle.invRotate
              (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)) ⟶
          Triangle.obj₂.{v, u}
            (Triangle.invRotate
              (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)))

Tactic:
simp
-- 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
X : C
⊢ (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).mor₂ ≫
      Iso.hom (Iso.refl (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).obj₃) =
    Iso.hom (Iso.refl (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).obj₂) ≫
      Triangle.mor₂
        (Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0))

Tactic:
simp
-- 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
X : C
dsimp :
  𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) X) =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
      𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
⊢ (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X)) =
    Iso.hom (Iso.refl (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X))).obj₃) ≫
      Triangle.mor₃
        (Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0))

Tactic:
dsimp
-- 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
X : C
⊢ 𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) X) =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
      𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)

Tactic:
simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp]

Premises used: CategoryTheory.shift_shiftFunctorCompIsoId_inv_app, CategoryTheory.Category.id_comp
-- 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
X : C
⊢ Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) ≅
    Triangle.invRotate (Triangle.mk (X := 0) 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)) 0)

Tactic:
exact Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _)
    (by simp) (by simp)
    (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- 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} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
obtain :
  ∀ (g : T.obj₃ ⟶ obj₃.{v, u} (mk (X := 0) 0 (𝟙 X) 0)) (hg₁ : T.mor₂ ≫ g = f ≫ mor₂ (mk (X := 0) 0 (𝟙 X) 0)),
    T.mor₃ ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) 0 = g ≫ mor₃ (mk (X := 0) 0 (𝟙 X) 0) →
      ∃ (g : T.obj₃ ⟶ X), f = T.mor₂ ≫ g
⊢ ∃ (g : T.obj₃ ⟶ X), f = T.mor₂ ≫ g

Tactic:
obtain ⟨g, ⟨hg₁, _⟩⟩ := complete_distinguished_triangle_morphism T _ hT
    (contractible_distinguished₁ X) 0 f (by cat_disch)

Premises used: CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, OfNat.ofNat, CategoryTheory.Pretriangulated.contractible_distinguished₁
-- 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} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ obj₃.{v, u} (mk (X := 0) 0 (𝟙 X) 0)
hg₁ : T.mor₂ ≫ g = f ≫ mor₂ (mk (X := 0) 0 (𝟙 X) 0)
right : T.mor₃ ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) 0 = g ≫ mor₃ (mk (X := 0) 0 (𝟙 X) 0)
⊢ f = T.mor₂ ≫ g

Tactic:
simpa using hg₁.symm

Premises used: Eq.symm
-- 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} (CategoryTheory.shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ obj₃.{v, u} (mk (X := 0) 0 (𝟙 X) 0)
hg₁ : T.mor₂ ≫ g = f ≫ mor₂ (mk (X := 0) 0 (𝟙 X) 0)
right : T.mor₃ ≫ Functor.map (CategoryTheory.shiftFunctor C (A := ℤ) 1) 0 = g ≫ mor₃ (mk (X := 0) 0 (𝟙 X) 0)
⊢ ∃ (g : T.obj₃ ⟶ X), f = T.mor₂ ≫ g

Tactic:
exact ⟨g, by simpa using hg₁.symm⟩