awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
refine :
  Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) 1)
      (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ≅
    Triangle.mk H.m₁ H.m₃
      ((-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk α β γ).mor₁) ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk (ι.map f₁) f₂ f₃).mor₃)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) 1)
      (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate)

Tactic:
refine isomorphic_distinguished _ H.mem _ ?_

Premises used: CategoryTheory.Triangulated.Octahedron.mem, CategoryTheory.Pretriangulated.isomorphic_distinguished
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
⊢ Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (A := ℤ) 1)
      (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃)).rotate ≅
    Triangle.mk H.m₁ H.m₃
      ((-Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk α β γ).mor₁) ≫
        Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk (ι.map f₁) f₂ f₃).mor₃)

Tactic:
exact Triangle.isoMk _ _ (-(Iso.refl _)) (Iso.refl _) (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃))

Tactic:
have Hmem : Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃) ∈ distTriang C := by
      rw [rotate_distinguished_triangle, ← Triangle.shift_distinguished_iff _ 1]
      refine isomorphic_distinguished _ H.mem _ ?_
      exact Triangle.isoMk _ _ (-(Iso.refl _)) (Iso.refl _) (Iso.refl _)
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
Hmem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃))
⊢ (ι ⋙ shiftFunctor C (A := ℤ) 1).map (m₁ ≫ i) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map f₁

Tactic:
simpa [hm₁] using H.comm₂

Premises used: CategoryTheory.Triangulated.Octahedron.comm₂
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
hA : admissibleMorphism ι = ⊤
inst_12 : IsTriangulated.{v_1, u_1} C
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
this_1 : admissibleMorphism ι f₁
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
this : Epi (πQ f₂ β)
I : A
i : I ⟶ X₂
δ : ι.obj Q ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj I)
hI :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map i) (ι.map (πQ f₂ β)) δ)
H : Octahedron ⋯ ⋯ ⋯ ⋯
m₁ : X₁ ⟶ I
hm₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map m₁) = H.m₁
m₃ : ι.obj I ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)
hm₃ : Functor.map (shiftFunctor C (A := ℤ) 1) m₃ = H.m₃
Hmem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map (ιK f₃ α)) (ι.map m₁) (-m₃))
⊢ Nonempty (Abelian.AbelianStruct f₁)

Tactic:
exact ⟨{
      kernelFork := _
      isLimitKernelFork := isLimitKernelFork hι hT hT'
      cokernelCofork := _
      isColimitCokernelCofork := isColimitCokernelCofork hι hT hT'
      image := _
      imageι := _
      imageπ := _
      ι_imageπ := _
      imageι_π := _
      imageIsCokernel := isColimitCokernelCoforkOfDistTriang hι _ _ _ Hmem
      imageIsKernel := isLimitKernelForkOfDistTriang hι _ _ _ hI
      fac := (ι ⋙ shiftFunctor C (1 : ℤ)).map_injective (by simpa [hm₁] using H.comm₂) }⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
obtain :
  ∀ (X Y : C) (hX : t.le 0 X) (hY : t.ge 1 Y) (f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A)
    (g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y)
    (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (mem :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk f g h)),
    ∃ (X : C) (Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y) (h :
      Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
        (Triangle.mk f g h)
⊢ ∃ (X : C) (Y : C) (_ : t.le n₀ X) (_ : t.ge n₁ Y) (f : X ⟶ A) (g : A ⟶ Y) (h :
    Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      (Triangle.mk f g h)

Tactic:
obtain ⟨X, Y, hX, hY, f, g, h, mem⟩ := t.exists_triangle_zero_one (A⟦n₀⟧)

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Triangulated.TStructure.exists_triangle_zero_one, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃)

Tactic:
isomorphic_distinguished _ (Triangle.shift_distinguished _ mem (-n₀)) _ ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.shift_distinguished, CategoryTheory.Pretriangulated.isomorphic_distinguished, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
refine :
  Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ≅
    Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃)

Tactic:
refine isomorphic_distinguished _ (Triangle.shift_distinguished _ mem (-n₀)) _ ?_

Premises used: CategoryTheory.Pretriangulated.Triangle.shift_distinguished, CategoryTheory.Pretriangulated.isomorphic_distinguished, Neg.neg
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
refine_1 :
  (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₁ ≫ e.symm.hom =
    Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁) ≫
      (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₁
refine_2 :
  (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₂ ≫
      Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃) =
    e.symm.hom ≫ (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₂
refine_3 :
  (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁)) =
    Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃) ≫
      (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₃
⊢ Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃ ≅
    Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _) ?_ ?_ ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
⊢ (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₁ ≫ e.symm.hom =
    Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁) ≫
      (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₁

Tactic:
simp [T]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
⊢ (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₂ ≫
      Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃) =
    e.symm.hom ≫ (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₂

Tactic:
simp [T]
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
A : C
n₀ n₁ : ℤ
h_1 : n₀ + 1 = n₁
X Y : C
hX : t.le 0 X
hY : t.ge 1 Y
f : X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A
g : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) A ⟶ Y
h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk f g h)
T : Triangle.{v_1, u_1} C := Functor.obj (Triangle.shiftFunctor C (-n₀)) (Triangle.mk f g h)
e : Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n₀) ⋙ Equivalence.inverse (shiftEquiv C n₀)) A ≅
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) A :=
  Iso.app (Iso.symm (Equivalence.unitIso (shiftEquiv C n₀))) A
⊢ (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1)
        (Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₁)) =
    Iso.hom (Iso.refl (Triangle.mk (T.mor₁ ≫ e.hom) (e.inv ≫ T.mor₂) T.mor₃).obj₃) ≫
      (Functor.obj (shiftFunctor (Triangle.{v_1, u_1} C) (-n₀)) (Triangle.mk f g h)).mor₃

Tactic:
simp [T]