awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
φ : A ⟶ B
inst_2 : IsIso φ
⊢ IsIso φ.hom₁

Tactic:
(inferInstance : IsIso (π₁.map φ))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
φ : A ⟶ B
inst_2 : IsIso φ
⊢ IsIso φ.hom₂

Tactic:
(inferInstance : IsIso (π₂.map φ))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ A B : Triangle.{v, u} C
φ : A ⟶ B
inst_2 : IsIso φ
⊢ IsIso φ.hom₃

Tactic:
(inferInstance : IsIso (π₃.map φ))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
h₁ :
  (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₁ =
    TriangleMorphism.hom₁
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)
h₂ :
  (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₂ =
    TriangleMorphism.hom₂
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)
h₃ :
  (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₃ =
    TriangleMorphism.hom₃
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)
⊢ A.map φ ≫
      { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x_1) (B.obj x_1) } =
    { hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
        TriangleMorphism (A.obj x) (B.obj x) } ≫
      B.map φ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
⊢ (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₁ =
    TriangleMorphism.hom₁
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)

Tactic:
hom₁.naturality φ

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
⊢ (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₁ =
    TriangleMorphism.hom₁
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)

Tactic:
exact hom₁.naturality φ

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
⊢ (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₂ =
    TriangleMorphism.hom₂
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)

Tactic:
hom₂.naturality φ

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
⊢ (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₂ =
    TriangleMorphism.hom₂
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)

Tactic:
exact hom₂.naturality φ

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
⊢ (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₃ =
    TriangleMorphism.hom₃
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)

Tactic:
hom₃.naturality φ

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C (A := ℤ) 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x x_1 : J
φ : x ⟶ x_1
⊢ (A.map φ ≫
        { hom₁ := hom₁.app x_1, hom₂ := hom₂.app x_1, hom₃ := hom₃.app x_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x_1) (B.obj x_1) }).hom₃ =
    TriangleMorphism.hom₃
      ({ hom₁ := hom₁.app x, hom₂ := hom₂.app x, hom₃ := hom₃.app x, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ :
          TriangleMorphism (A.obj x) (B.obj x) } ≫
        B.map φ)

Tactic:
exact hom₃.naturality φ

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C (A := ℤ) 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₁Toπ₂ ≫ iso₂.inv = iso₁.inv ≫ A.whiskerLeft π₁Toπ₂

Tactic:
simp only [← cancel_epi iso₁.hom, ← reassoc_of% comm₁,
          Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C (A := ℤ) 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₂Toπ₃ ≫ iso₃.inv = iso₂.inv ≫ A.whiskerLeft π₂Toπ₃

Tactic:
simp only [← cancel_epi iso₂.hom, ← reassoc_of% comm₂,
          Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C (A := ℤ) 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
simp : A.whiskerLeft π₃Toπ₁ ≫ 𝟙 ((A ⋙ π₁) ⋙ shiftFunctor C (A := ℤ) 1) = A.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.inv (shiftFunctor C (A := ℤ) 1) = iso₃.inv ≫ A.whiskerLeft π₃Toπ₁

Tactic:
simp only [← cancel_epi iso₃.hom, ← reassoc_of% comm₃, Iso.hom_inv_id_assoc,
        ← whiskerRight_comp, Iso.hom_inv_id, whiskerRight_id']

Premises used: CategoryTheory.Functor.whiskerRight_id', CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.whiskerRight_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasShift.{v, u, 0} C ℤ
T₁ T₂ T₃ : Triangle.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
A B : J ⥤ Triangle.{v, u} C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C (A := ℤ) 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ A.whiskerLeft π₃Toπ₁ ≫ 𝟙 ((A ⋙ π₁) ⋙ shiftFunctor C (A := ℤ) 1) = A.whiskerLeft π₃Toπ₁

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
dsimp : F.map X.mor₁ ≫ F.map f.hom₂ = F.map f.hom₁ ≫ F.map Y.mor₁
⊢ Eq (α :=
    Triangle.obj₁
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ⟶
      Triangle.obj₂
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))
    (Triangle.mor₁
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ≫
      F.map f.hom₂)
    (F.map f.hom₁ ≫
      Triangle.mor₁
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
⊢ F.map X.mor₁ ≫ F.map f.hom₂ = F.map f.hom₁ ≫ F.map Y.mor₁

Tactic:
simp only [← F.map_comp, f.comm₁]

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.comm₁, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
dsimp : F.map X.mor₂ ≫ F.map f.hom₃ = F.map f.hom₂ ≫ F.map Y.mor₂
⊢ Eq (α :=
    Triangle.obj₂
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ⟶
      Triangle.obj₃
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))
    (Triangle.mor₂
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ≫
      F.map f.hom₃)
    (F.map f.hom₂ ≫
      Triangle.mor₂
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
⊢ F.map X.mor₂ ≫ F.map f.hom₃ = F.map f.hom₂ ≫ F.map Y.mor₂

Tactic:
simp only [← F.map_comp, f.comm₂]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
dsimp :
  Eq (α := F.obj X.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F.obj Y.obj₁))
    ((F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁) ≫ map (shiftFunctor D (A := ℤ) 1) (F.map f.hom₁))
    (F.map f.hom₃ ≫ F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)
⊢ Eq (α :=
    Triangle.obj₃
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1)
        (Triangle.obj₁
          (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂)
            (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁))))
    (Triangle.mor₃
        (Triangle.mk (F.map X.mor₁) (F.map X.mor₂) (F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁)) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map f.hom₁))
    (F.map f.hom₃ ≫
      Triangle.mor₃
        (Triangle.mk (F.map Y.mor₁) (F.map Y.mor₂) (F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)))

Tactic:
dsimp [Functor.comp]

Premises used: CategoryTheory.Functor.comp
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
X Y : Triangle.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := F.obj X.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (F.obj Y.obj₁))
    ((F.map X.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) X.obj₁) ≫ map (shiftFunctor D (A := ℤ) 1) (F.map f.hom₁))
    (F.map f.hom₃ ≫ F.map Y.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) Y.obj₁)

Tactic:
simp only [Category.assoc, ← NatTrans.naturality,
          ← F.map_comp_assoc, f.comm₃]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
h₁ : f.hom₁ = g.hom₁
h₂ : f.hom₂ = g.hom₂
h₃ : f.hom₃ = g.hom₃
⊢ f = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
h₁ : F.map f.hom₁ = F.map g.hom₁
⊢ f.hom₁ = g.hom₁

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
h₂ : F.map f.hom₂ = F.map g.hom₂
⊢ f.hom₂ = g.hom₂

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
h₃ : F.map f.hom₃ = F.map g.hom₃
⊢ f.hom₃ = g.hom₃

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ F.map f.hom₁ = F.map g.hom₁

Tactic:
congr_arg TriangleMorphism.hom₁ h

Premises used: congr_arg, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ F.map f.hom₁ = F.map g.hom₁

Tactic:
exact congr_arg TriangleMorphism.hom₁ h

Premises used: congr_arg, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁
-- Module: Mathlib.CategoryTheory.Triangulated.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : HasShift.{v_2, u_2, 0} D ℤ
inst_5 : HasShift.{v_3, u_3, 0} E ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_6 : F.CommShift ℤ
G : Functor.{v_2, v_3, u_2, u_3} D E
inst_7 : G.CommShift ℤ
inst_8 : F.Faithful
X Y : Triangle.{v_1, u_1} C
f g : X ⟶ Y
h :
  Eq (α := Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj F.mapTriangle X) (obj F.mapTriangle Y)) (map F.mapTriangle f)
    (map F.mapTriangle g)
⊢ F.map f.hom₂ = F.map g.hom₂

Tactic:
congr_arg TriangleMorphism.hom₂ h

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, congr_arg