awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_15 : F.CommShift ℤ
inst_16 : F.IsTriangulated
inst_17 : F.Full
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _) T
X₁ : C
e₁ : F.obj X₁ ≅ T.obj₁
X₃ : C
e₃ : F.obj X₃ ≅ T.obj₃
h : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
hh :
  F.map h =
    e₃.hom ≫
      T.mor₃ ≫ Functor.map (shiftFunctor D (A := ℤ) 1) e₁.inv ≫ NatTrans.app (Iso.inv (Functor.commShiftIso F 1)) X₁
X₂ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
⊢ F.essImage T.obj₂

Tactic:
exact ⟨X₂, ⟨Triangle.π₂.mapIso
      (isoTriangleOfIso₁₃ _ _ (F.map_distinguished _ H) hT e₁ e₃
        (by simp [hh, ← Functor.map_comp]))⟩⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
F : Functor.{v_3, v_1, u_3, u_1} E C
hF : ∀ (X : E), P (F.obj X)
inst_15 : Preadditive.{v_3, u_3} E
inst_16 : F.CommShift ℤ
inst_17 : HasZeroObject.{v_3, u_3} E
inst_18 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 rw : F.IsTriangulated
⊢ (P.lift F hF).IsTriangulated

Tactic:
rw [Functor.isTriangulated_iff_comp_right (P.liftCompιIso F hF)]

Premises used: CategoryTheory.ObjectProperty.liftCompιIso, CategoryTheory.Functor.isTriangulated_iff_comp_right
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
F : Functor.{v_3, v_1, u_3, u_1} E C
hF : ∀ (X : E), P (F.obj X)
inst_15 : Preadditive.{v_3, u_3} E
inst_16 : F.CommShift ℤ
inst_17 : HasZeroObject.{v_3, u_3} E
inst_18 : ∀ (n : ℤ), Functor.Additive.{v_3, u_3, v_3, u_3} (shiftFunctor E n)
inst_19 : Pretriangulated.{v_3, u_3} E
inst_20 : F.IsTriangulated
⊢ F.IsTriangulated

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D_1 : Type u_2
inst_6 : Category.{v_2, u_2} D_1
inst_7 : Preadditive.{v_2, u_2} D_1
inst_8 : HasZeroObject.{v_2, u_2} D_1
inst_9 : HasShift.{v_2, u_2, 0} D_1 ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D_1 n)
inst_11 : Pretriangulated.{v_2, u_2} D_1
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
D : Type u_4
inst_15 : Category.{u_5, u_4} D
inst_16 : HasZeroObject.{u_5, u_4} D
inst_17 : Preadditive.{u_5, u_4} D
inst_18 : HasShift.{u_5, u_4, 0} D ℤ
inst_19 : ∀ (n : ℤ), Functor.Additive.{u_5, u_4, u_5, u_4} (shiftFunctor D n)
inst_20 : Pretriangulated.{u_5, u_4} D
F : Functor.{v_1, u_5, u_1, u_4} C D
inst_21 : F.CommShift ℤ
inst_22 : F.IsTriangulated
inst_23 : F.Full
rw : (P.ι ⋙ F).essImage.IsTriangulated
⊢ (P.map F).IsTriangulated

Tactic:
rw [← F.essImage_ι_comp]

Premises used: CategoryTheory.Functor.essImage_ι_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Subcategory
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D_1 : Type u_2
inst_6 : Category.{v_2, u_2} D_1
inst_7 : Preadditive.{v_2, u_2} D_1
inst_8 : HasZeroObject.{v_2, u_2} D_1
inst_9 : HasShift.{v_2, u_2, 0} D_1 ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D_1 n)
inst_11 : Pretriangulated.{v_2, u_2} D_1
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
D : Type u_4
inst_15 : Category.{u_5, u_4} D
inst_16 : HasZeroObject.{u_5, u_4} D
inst_17 : Preadditive.{u_5, u_4} D
inst_18 : HasShift.{u_5, u_4, 0} D ℤ
inst_19 : ∀ (n : ℤ), Functor.Additive.{u_5, u_4, u_5, u_4} (shiftFunctor D n)
inst_20 : Pretriangulated.{u_5, u_4} D
F : Functor.{v_1, u_5, u_1, u_4} C D
inst_21 : F.CommShift ℤ
inst_22 : F.IsTriangulated
inst_23 : F.Full
⊢ (P.ι ⋙ F).essImage.IsTriangulated

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_4 : 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
X Y : A
n : ℤ
f : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
rw :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n) ⋙ Equivalence.inverse (shiftEquiv C n))
          (ι.obj X))
        (NatTrans.app (Iso.hom (Equivalence.unitIso (shiftEquiv C n))) (ι.obj X))
        (Functor.map (shiftFunctor C (-n)) f) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
    (0 :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
    (Functor.map (shiftFunctor C (-n)) f) (Functor.map (shiftFunctor C (-n)) 0)

Tactic:
rw [← cancel_epi ((shiftEquiv C n).unitIso.hom.app _), Functor.map_zero, comp_zero]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.shiftEquiv, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_4 : 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
X Y : A
n : ℤ
f : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ -n < 0

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_4 : 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
X Y : A
n : ℤ
f : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n) ⋙ Equivalence.inverse (shiftEquiv C n))
          (ι.obj X))
        (NatTrans.app (Iso.hom (Equivalence.unitIso (shiftEquiv C n))) (ι.obj X))
        (Functor.map (shiftFunctor C (-n)) f) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
    (0 :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))

Tactic:
exact hι _ (by lia)
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
X₁ : A
X₃ : C
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
K : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
inst_3 : ι.Full
⊢ Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map (ιK f₃ α)) = α ≫ f₃

Tactic:
(ι ⋙ shiftFunctor C (1 : ℤ)).map_preimage _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.shiftFunctor, CategoryTheory.Triangulated.AbelianSubcategory.ιK, OfNat.ofNat, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
X₂ : A
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
Q : A
β : X₃ ⟶ ι.obj Q
inst_2 : ι.Full
⊢ ι.map (πQ f₂ β) = f₂ ≫ β

Tactic:
ι.map_preimage _

Premises used: CategoryTheory.Triangulated.AbelianSubcategory.πQ, CategoryTheory.Functor.map_preimage
-- 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
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₃)
K : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
⊢ (Triangle.mk (ι.map f₁) f₂ f₃).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk (ι.map f₁) f₂ f₃).mor₁ = 0

Tactic:
have := comp_distTriang_mor_zero₃₁ _ hT
-- 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
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₃)
K : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
this : f₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map f₁) = 0
⊢ (ι ⋙ shiftFunctor C (A := ℤ) 1).map (ιK f₃ α ≫ f₁) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0

Tactic:
simp [this]
-- 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
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₃)
Q : A
β : X₃ ⟶ ι.obj Q
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
⊢ (Triangle.mk (ι.map f₁) f₂ f₃).mor₁ ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ = 0

Tactic:
have := comp_distTriang_mor_zero₁₂ _ hT
-- 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
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₃)
Q : A
β : X₃ ⟶ ι.obj Q
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
this : ι.map f₁ ≫ f₂ = 0
⊢ ι.map (f₁ ≫ πQ f₂ β) = ι.map 0

Tactic:
simp [reassoc_of% this]
-- 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
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₃)
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 α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
rw : ∀ (P : A) (g : P ⟶ K), g ≫ ιK f₃ α = 0 → g = 0
⊢ Mono (ιK f₃ α)

Tactic:
rw [mono_iff_cancel_zero]

Premises used: CategoryTheory.Preadditive.mono_iff_cancel_zero
-- 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
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₃)
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 α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
k : B ⟶ K
hk : k ≫ ιK f₃ α = 0
⊢ (ι ⋙ shiftFunctor C (A := ℤ) 1).map (k ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0

Tactic:
replace hk := (ι ⋙ shiftFunctor C (1 : ℤ)).congr_map hk
-- 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
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₃)
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 α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
k : B ⟶ K
hk : (ι ⋙ shiftFunctor C (A := ℤ) 1).map (k ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
a : (ι ⋙ shiftFunctor C (A := ℤ) 1).map k = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
⊢ k = 0

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

Premises used: CategoryTheory.Functor.comp, CategoryTheory.shiftFunctor, CategoryTheory.Functor.map_injective, OfNat.ofNat
-- 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
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₃)
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 α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
k : B ⟶ K
hk : (ι ⋙ shiftFunctor C (A := ℤ) 1).map (k ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
a :
  ∀ (hk : (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α) ≫ f₃ = 0),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k)) 0
⊢ (ι ⋙ shiftFunctor C (A := ℤ) 1).map k = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, Functor.map_comp,
    shift_ι_map_ιK, Functor.map_zero, ← assoc] at hk ⊢

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map, CategoryTheory.Triangulated.AbelianSubcategory.shift_ι_map_ιK
-- 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
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₃)
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 α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
k : B ⟶ K
hk : (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α) ≫ f₃ = 0
a :
  ∀ (l : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂)
    (hl : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α = l ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
      (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k)) 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k)) 0

Tactic:
obtain ⟨l, hl⟩ := Triangle.coyoneda_exact₃ _ hT _ hk

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃