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
X Y : P.FullSubcategory
f : X ⟶ Y
Z' : C
g' : P.ι.obj Y ⟶ Z'
h' : Z' ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (P.ι.obj X)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (P.ι.map f) g' h')
Z'' : C
hZ'' : P Z''
e : (Triangle.mk (P.ι.map f) g' h').obj₃ ≅ Z''
⊢ ∃ (Z : P.FullSubcategory) (g : Y ⟶ Z) (h :
    Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
      (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
        (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
      (Triangle.mk f g h)

Tactic:
exact ⟨⟨Z'', hZ''⟩, P.fullyFaithfulι.preimage (g' ≫ e.hom),
      P.fullyFaithfulι.preimage (e.inv ≫ h' ≫ (P.ι.commShiftIso (1 : ℤ)).inv.app X),
      isomorphic_distinguished _ mem _ (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm)⟩
-- 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
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ Eq (α := Triangle.obj₁ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₂ (Functor.obj P.ι.mapTriangle T₂))
    (Triangle.mor₁ (Functor.obj P.ι.mapTriangle T₁) ≫ P.ι.map b)
    (P.ι.map a ≫ Triangle.mor₁ (Functor.obj P.ι.mapTriangle T₂))

Tactic:
simpa using P.ι.congr_map comm

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.congr_map
-- 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
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
obtain :
  ∀ (c : Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₂))
    (hc₁ :
      Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₁) ≫ c = P.ι.map b ≫ Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₂))
    (hc₂ :
      Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a) =
        c ≫ Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₂)),
    ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
      T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a = c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
obtain ⟨c, ⟨hc₁, hc₂⟩⟩ := complete_distinguished_triangle_morphism (P.ι.mapTriangle.obj T₁)
      (P.ι.mapTriangle.obj T₂) hT₁ hT₂ (P.ι.map a) (P.ι.map b)
      (by simpa using P.ι.congr_map comm)

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.map, CategoryTheory.Functor.mapTriangle, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, CategoryTheory.Functor.obj
-- 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
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₂)
hc₁ : Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₁) ≫ c = P.ι.map b ≫ Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₂)
hc₂ :
  Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a) =
    c ≫ Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₂)
refine : T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a = P.fullyFaithfulι.preimage c ≫ T₂.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a = c ≫ T₂.mor₃

Tactic:
refine ⟨P.fullyFaithfulι.preimage c, ⟨by cat_disch, ?_⟩⟩
-- 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
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₂)
hc₁ : Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₁) ≫ c = P.ι.map b ≫ Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₂)
hc₂ :
  Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a) =
    c ≫ Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₂)
h :
  (T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a).hom =
    (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a = P.fullyFaithfulι.preimage c ≫ T₂.mor₃

Tactic:
ext
-- 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
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₂)
hc₁ : Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₁) ≫ c = P.ι.map b ≫ Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₂)
hc₂ :
  Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a) =
    c ≫ Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₂)
⊢ Eq (α :=
    P.ι.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) T₁.obj₁) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (P.ι.obj T₂.obj₁))
    (P.ι.map (Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
    (NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₁.obj₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a))

Tactic:
have := P.ι.commShiftIso_hom_naturality a (1 : ℤ)
-- 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
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₂)
hc₁ : Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₁) ≫ c = P.ι.map b ≫ Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₂)
hc₂ :
  Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a) =
    c ≫ Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₂)
this :
  Eq (α :=
    P.ι.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) T₁.obj₁) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (P.ι.obj T₂.obj₁))
    (P.ι.map (Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
    (NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₁.obj₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a))
h :
  Eq (α := T₁.obj₃.obj (P := P) ⟶ (P.ι ⋙ shiftFunctor C (A := ℤ) 1).obj T₂.obj₁)
    ((T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a).hom ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
    ((P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom ≫ NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
⊢ (T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a).hom =
    (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom

Tactic:
rw [← cancel_mono ((Functor.commShiftIso P.ι (1 : ℤ)).hom.app T₂.obj₁)]

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.cancel_mono, OfNat.ofNat, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- 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
inst_15 : IsTriangulated.{v_1, u_1} C
⊢ IsTriangulated.{v_1, u_1} P.FullSubcategory

Tactic:
IsTriangulated.of_fully_faithful_triangulated_functor P.ι

Premises used: CategoryTheory.IsTriangulated.of_fully_faithful_triangulated_functor, CategoryTheory.ObjectProperty.ι
-- 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
n : ℤ
Y : D
X : C
e : F.obj X ≅ Y
⊢ F.essImage.shift n Y

Tactic:
⟨X⟦n⟧, ⟨(F.commShiftIso n).app _ ≪≫ (shiftFunctor D n).mapIso e⟩⟩

Premises used: CategoryTheory.ObjectProperty.shift, CategoryTheory.shiftFunctor, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- 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
n : ℤ
Y : D
X : C
e : F.obj X ≅ Y
⊢ F.essImage.shift n Y

Tactic:
exact ⟨X⟦n⟧, ⟨(F.commShiftIso n).app _ ≪≫ (shiftFunctor D n).mapIso e⟩⟩
-- 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₃
have :
  ∀ (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₁),
    F.essImage T.obj₂
⊢ F.essImage T.obj₂

Tactic:
have ⟨h, hh⟩ := F.map_surjective (e₃.hom ≫ T.mor₃ ≫ e₁.inv⟦1⟧' ≫
      (F.commShiftIso (1 : ℤ)).inv.app X₁)
-- 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₁
obtain :
  ∀ (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₂
⊢ F.essImage T.obj₂

Tactic:
obtain ⟨X₂, f, g, H⟩ := distinguished_cocone_triangle₂ h

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂
-- 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)
⊢ Triangle.mor₃ (Functor.obj F.mapTriangle (Triangle.mk f g h)) ≫ Functor.map (shiftFunctor D (A := ℤ) 1) e₁.hom =
    e₃.hom ≫ T.mor₃

Tactic:
simp [hh, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp