awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.LeftFraction X Y
hφ : g = φ.map (W := P.trW) L ⋯
α : X ⟶ Y
hα : (fun (f : X ⟶ Y) ↦ f ≫ φ.s (W := P.trW)) α = φ.f (W := P.trW)
refine_2 : L.map α = φ.map (W := P.trW) L ⋯
refine_2₁ : L.map α ≫ L.map (φ.s (W := P.trW)) = φ.map (W := P.trW) L ⋯ ≫ L.map (φ.s (W := P.trW))
refine_2₂ : L.map α ≫ L.map (φ.s (W := P.trW)) = L.map (φ.f (W := P.trW))
refine_2₃ : L.map α ≫ L.map (φ.s (W := P.trW)) = L.map ((fun (f : X ⟶ Y) ↦ f ≫ φ.s (W := P.trW)) α)
refine_2₄ refine_2₅ : L.map α ≫ L.map (φ.s (W := P.trW)) = L.map α ≫ L.map (φ.s (W := P.trW))
⊢ L.map α = g

Tactic:
rw [hφ, ← cancel_mono (L.map φ.s), MorphismProperty.LeftFraction.map_comp_map_s,
      ← hα, Functor.map_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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
e : T₁ ≅ T₂
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁ ↔
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂

Tactic:
⟨fun hT₁ => isomorphic_distinguished _ hT₁ _ e.symm,
    fun hT₂ => isomorphic_distinguished _ hT₂ _ e⟩

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, Iff.intro, CategoryTheory.Iso.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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
H : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T.rotate

Tactic:
(rotate_distinguished_triangle T).mp H

Premises used: Iff.mp, CategoryTheory.Pretriangulated.rotate_distinguished_triangle
-- 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 : Triangle.{v, u} C
H : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T.invRotate

Tactic:
(rotate_distinguished_triangle T.invRotate).mpr
    (isomorphic_distinguished T H T.invRotate.rotate (invRotCompRot.app T))

Premises used: Iff.mpr, CategoryTheory.Pretriangulated.Triangle.invRotate, CategoryTheory.Pretriangulated.Triangle.rotate, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Pretriangulated.invRotCompRot, CategoryTheory.Iso.app, CategoryTheory.Pretriangulated.rotate_distinguished_triangle
-- 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 : Triangle.{v, u} C
H : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
obtain :
  ∀ (c : Triangle.obj₃.{v, u} (contractibleTriangle T.obj₁) ⟶ T.obj₃)
    (hc :
      Triangle.mor₂ (contractibleTriangle T.obj₁) ≫ c = T.mor₁ ≫ T.mor₂ ∧
        Triangle.mor₃ (contractibleTriangle T.obj₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 T.obj₁) = c ≫ T.mor₃),
    T.mor₁ ≫ T.mor₂ = 0
⊢ T.mor₁ ≫ T.mor₂ = 0

Tactic:
obtain ⟨c, hc⟩ :=
    complete_distinguished_triangle_morphism _ _ (contractible_distinguished T.obj₁) H (𝟙 T.obj₁)
      T.mor₁ rfl

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.CategoryStruct.id, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, CategoryTheory.Pretriangulated.Triangle.mor₁, CategoryTheory.Pretriangulated.contractible_distinguished, rfl
-- 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 : Triangle.{v, u} C
H : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
c : Triangle.obj₃.{v, u} (contractibleTriangle T.obj₁) ⟶ T.obj₃
hc :
  Triangle.mor₂ (contractibleTriangle T.obj₁) ≫ c = T.mor₁ ≫ T.mor₂ ∧
    Triangle.mor₃ (contractibleTriangle T.obj₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ T.mor₂ = 0

Tactic:
simpa only [contractibleTriangle_mor₂, zero_comp] using hc.left.symm

Premises used: CategoryTheory.Pretriangulated.contractibleTriangle_mor₂, And.left, CategoryTheory.Limits.zero_comp, 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} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
H : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ T.mor₂ ≫ T.mor₃ = 0

Tactic:
comp_distTriang_mor_zero₁₂ T.rotate (rot_of_distTriang T H)

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, CategoryTheory.Pretriangulated.Triangle.rotate, CategoryTheory.Pretriangulated.rot_of_distTriang
-- 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 : Triangle.{v, u} C
H : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T.rotate.rotate

Tactic:
have H₂ := rot_of_distTriang T.rotate (rot_of_distTriang T H)
-- 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 : Triangle.{v, u} C
H : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
H₂ :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T.rotate.rotate
⊢ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) T.mor₁ = 0

Tactic:
simpa using comp_distTriang_mor_zero₁₂ T.rotate.rotate H₂

Premises used: CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, CategoryTheory.Pretriangulated.Triangle.rotate
-- 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
Y Z : C
g : Y ⟶ Z
obtain :
  ∀ (X' : C) (f' : Z ⟶ X') (g' : X' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y)
    (mem :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk g f' g')),
    ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)
⊢ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)

Tactic:
obtain ⟨X', f', g', mem⟩ := distinguished_cocone_triangle g

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- 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
Y Z : C
g : Y ⟶ Z
X' : C
f' : Z ⟶ X'
g' : X' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f' g')
⊢ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)

Tactic:
⟨_, _, _, inv_rot_of_distTriang _ mem⟩

Premises used: CategoryTheory.Pretriangulated.inv_rot_of_distTriang, 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
Y Z : C
g : Y ⟶ Z
X' : C
f' : Z ⟶ X'
g' : X' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk g f' g')
⊢ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)

Tactic:
exact ⟨_, _, _, inv_rot_of_distTriang _ mem⟩
-- 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
Z X : C
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
obtain :
  ∀ (Y' : C) (f' : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X ⟶ Y')
    (g' : Y' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Z)
    (mem :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk h f' g')),
    ∃ (Y : C) (f : X ⟶ Y) (g : Y ⟶ Z),
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f g h)
⊢ ∃ (Y : C) (f : X ⟶ Y) (g : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)

Tactic:
obtain ⟨Y', f', g', mem⟩ := distinguished_cocone_triangle h

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- 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
Z X : C
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
Y' : C
f' : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X ⟶ Y'
g' : Y' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Z
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk h f' g')
T' : Triangle.{v, u} C := (Triangle.mk h f' g').invRotate.invRotate
⊢ ∃ (Y : C) (f : X ⟶ Y) (g : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)

Tactic:
⟨T'.obj₂, ((shiftEquiv C (1 : ℤ)).unitIso.app X).hom ≫ T'.mor₁, T'.mor₂,
    isomorphic_distinguished _ (inv_rot_of_distTriang _ (inv_rot_of_distTriang _ mem)) _ ?_⟩

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.shiftEquiv, CategoryTheory.Pretriangulated.Triangle.mor₂, CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pretriangulated.Triangle.obj₂, CategoryTheory.Iso.app, CategoryTheory.Pretriangulated.Triangle.mor₁, OfNat.ofNat, CategoryTheory.Iso.hom
-- 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
Z X : C
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
Y' : C
f' : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X ⟶ Y'
g' : Y' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Z
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk h f' g')
T' : Triangle.{v, u} C := (Triangle.mk h f' g').invRotate.invRotate
refine :
  Triangle.mk (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X) ≫ T'.mor₁) T'.mor₂ h ≅
    (Triangle.mk h f' g').invRotate.invRotate
⊢ ∃ (Y : C) (f : X ⟶ Y) (g : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)

Tactic:
refine ⟨T'.obj₂, ((shiftEquiv C (1 : ℤ)).unitIso.app X).hom ≫ T'.mor₁, T'.mor₂,
    isomorphic_distinguished _ (inv_rot_of_distTriang _ (inv_rot_of_distTriang _ mem)) _ ?_⟩
-- 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
Z X : C
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
Y' : C
f' : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X ⟶ Y'
g' : Y' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Z
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk h f' g')
T' : Triangle.{v, u} C := (Triangle.mk h f' g').invRotate.invRotate
dsimp :
  h ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) X) =
    𝟙 Z ≫
      h ≫
        NatTrans.app (Iso.inv (shiftFunctorCompIsoId C (-1) 1 ⋯))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X)
⊢ (Triangle.mk (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X) ≫ T'.mor₁) T'.mor₂ h).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X)) =
    Iso.hom
        (Iso.refl
          (Triangle.mk (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X) ≫ T'.mor₁) T'.mor₂
              h).obj₃) ≫
      (Triangle.mk h f' g').invRotate.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
Z X : C
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
Y' : C
f' : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X ⟶ Y'
g' : Y' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Z
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk h f' g')
T' : Triangle.{v, u} C := (Triangle.mk h f' g').invRotate.invRotate
⊢ h ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (NatTrans.app (Iso.inv (shiftFunctorCompIsoId C 1 (-1) ⋯)) X) =
    𝟙 Z ≫
      h ≫
        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
Z X : C
h : Z ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X
Y' : C
f' : Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X ⟶ Y'
g' : Y' ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Z
mem :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk h f' g')
T' : Triangle.{v, u} C := (Triangle.mk h f' g').invRotate.invRotate
⊢ Triangle.mk (Iso.hom (Iso.app (Equivalence.unitIso (shiftEquiv C (A := ℤ) 1)) X) ≫ T'.mor₁) T'.mor₂ h ≅
    (Triangle.mk h f' g').invRotate.invRotate

Tactic:
exact Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _)
    (by cat_disch) (by cat_disch)
    (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} (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₂
obtain :
  ∀ (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₃),
    ∃ (a : T₁.obj₁ ⟶ T₂.obj₁),
      T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ ∃ (a : T₁.obj₁ ⟶ T₂.obj₁),
    T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
    (rot_of_distTriang _ hT₁) (rot_of_distTriang _ hT₂) b c comm

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

Tactic:
⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.shiftFunctor, And.intro, Exists.intro, OfNat.ofNat
-- 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₃
refine_1 : T₁.mor₁ ≫ b = Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁
refine_2 :
  T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Functor.preimage (shiftFunctor C (A := ℤ) 1) a) = c ≫ T₂.mor₃
⊢ ∃ (a : T₁.obj₁ ⟶ T₂.obj₁),
    T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
refine ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩
-- 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₃
refine_1 :
  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₁))
⊢ T₁.mor₁ ≫ b = Functor.preimage (shiftFunctor C (A := ℤ) 1) a ≫ T₂.mor₁

Tactic:
apply (shiftFunctor C (1 : ℤ)).map_injective

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_injective, OfNat.ofNat