awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
obtain : ∀ (h : A ⟶ T'.invRotate.obj₁) (hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁), g ≫ T.mor₁ = 0
⊢ g ≫ T.mor₁ = 0

Tactic:
obtain ⟨h, hh⟩ := Triangle.coyoneda_exact₂ T'.invRotate (inv_rot_of_distTriang _ hT')
      (g ≫ φ.hom₁) (by dsimp; rw [assoc, ← φ.comm₁, hf])

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, CategoryTheory.Pretriangulated.Triangle.invRotate, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
⊢ ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g

Tactic:
⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, OfNat.ofNat, Neg.neg, CategoryTheory.Pretriangulated.TriangleMorphism.hom₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
refine : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
⊢ ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g

Tactic:
refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
⊢ (Functor.obj (invRotate C) T).mor₁ ≫ TriangleMorphism.hom₂ (Functor.map (invRotate C) φ) =
    TriangleMorphism.hom₁ (Functor.map (invRotate C) φ) ≫ (Functor.obj (invRotate C) T').mor₁

Tactic:
have eq := ((invRotate C).map φ).comm₁
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁
rw : ((h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁) ≫ φ.hom₁ = g ≫ φ.hom₁
rw₁ : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
rw₂ : h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
rw₃ :
  h ≫
      inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁ =
    g ≫ φ.hom₁
rw₄ : h ≫ T'.invRotate.mor₁ = g ≫ φ.hom₁
rw₅ rw₆ : h ≫ T'.invRotate.mor₁ = h ≫ T'.invRotate.mor₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g

Tactic:
rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁, CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
obtain :
  ∀ (k : A ⟶ T.invRotate.obj₁) (hf : (k ≫ T.invRotate.mor₁) ≫ T.mor₁ ≫ φ.hom₂ = 0)
    (hh : (k ≫ T.invRotate.mor₁) ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁), (k ≫ T.invRotate.mor₁) ≫ T.mor₁ = 0
⊢ g ≫ T.mor₁ = 0

Tactic:
obtain ⟨k, rfl⟩ : ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g := by
      refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
      have eq := ((invRotate C).map φ).comm₁
      dsimp only [invRotate] at eq
      rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.Pretriangulated.Triangle.invRotate, CategoryTheory.Pretriangulated.Triangle.mor₁, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
h : A ⟶ T'.invRotate.obj₁
k : A ⟶ T.invRotate.obj₁
hf : (k ≫ T.invRotate.mor₁) ≫ T.mor₁ ≫ φ.hom₂ = 0
hh : (k ≫ T.invRotate.mor₁) ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
erw : k ≫ T.invRotate.mor₁ ≫ T.mor₁ = 0
erw₁ : Eq (α := A ⟶ T.obj₂) (k ≫ 0) 0
erw₂ erw₃ : Eq.{v + 1} (α := A ⟶ T.obj₂) 0 0
⊢ (k ≫ T.invRotate.mor₁) ≫ T.mor₁ = 0

Tactic:
erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, CategoryTheory.Limits.comp_zero, CategoryTheory.Pretriangulated.inv_rot_of_distTriang
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
⊢ Mono φ.hom₂

Tactic:
have : Mono φ.hom₂ := by
    rw [mono_iff_cancel_zero]
    intro A f hf
    obtain ⟨g, rfl⟩ := Triangle.coyoneda_exact₂ _ hT f
      (by rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp])
    rw [assoc] at hf
    obtain ⟨h, hh⟩ := Triangle.coyoneda_exact₂ T'.invRotate (inv_rot_of_distTriang _ hT')
      (g ≫ φ.hom₁) (by dsimp; rw [assoc, ← φ.comm₁, hf])
    obtain ⟨k, rfl⟩ : ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g := by
      refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
      have eq := ((invRotate C).map φ).comm₁
      dsimp only [invRotate] at eq
      rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
    erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
⊢ IsIso φ.hom₂

Tactic:
isIso_of_yoneda_map_bijective _ (fun A => ⟨?_, ?_⟩)

Premises used: CategoryTheory.isIso_of_yoneda_map_bijective, And.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
refine_1 : ∀ (A : C), Function.Injective (β := A ⟶ T'.obj₂) fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂
refine_2 : ∀ (A : C), Function.Surjective (β := A ⟶ T'.obj₂) fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂
⊢ IsIso φ.hom₂

Tactic:
refine isIso_of_yoneda_map_bijective _ (fun A => ⟨?_, ?_⟩)

Premises used: CategoryTheory.isIso_of_yoneda_map_bijective, And.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
f₁ f₂ : A ⟶ T.obj₂
h : Eq.{v + 1} (α := A ⟶ T'.obj₂) ((fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) f₁) ((fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) f₂)
⊢ f₁ = f₂

Tactic:
simpa only [← cancel_mono φ.hom₂] using h

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
⊢ (y₂ ≫ T'.mor₂ ≫ inv φ.hom₃) ≫ φ.hom₃ = y₂ ≫ T'.mor₂

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
refine_2 :
  ∀ (x₃ : A ⟶ T.obj₃) (hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂), ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂

Tactic:
obtain ⟨x₃, hx₃⟩ : ∃ (x₃ : A ⟶ T.obj₃), x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂ :=
      ⟨y₂ ≫ T'.mor₂ ≫ inv φ.hom₃, by simp⟩

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₃, CategoryTheory.Pretriangulated.Triangle.mor₂, CategoryTheory.Pretriangulated.TriangleMorphism.hom₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₁ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
rw₂ : x₃ ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0
rw₃ : x₃ ≫ φ.hom₃ ≫ T'.mor₃ = 0
rw₄ : y₂ ≫ T'.mor₂ ≫ T'.mor₃ = 0
rw₅ : Eq (α := A ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T'.obj₁) (y₂ ≫ 0) 0
rw₆ rw₇ : Eq.{v + 1} (α := A ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T'.obj₁) 0 0
⊢ x₃ ≫ T.mor₃ = 0

Tactic:
rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        comp_distTriang_mor_zero₂₃ _ hT', comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Pretriangulated.TriangleMorphism.comm₃, CategoryTheory.Limits.comp_zero, CategoryTheory.shiftFunctor, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁, CategoryTheory.Limits.zero_comp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
refine_2 : ∀ (x₂ : A ⟶ T.obj₂) (hx₂ : x₃ = x₂ ≫ T.mor₂), ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂

Tactic:
obtain ⟨x₂, hx₂⟩ := Triangle.coyoneda_exact₃ _ hT x₃
      (by rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        comp_distTriang_mor_zero₂₃ _ hT', comp_zero])

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₃
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
rw : y₂ ≫ T'.mor₂ - (x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0
rw₁ : y₂ ≫ T'.mor₂ - x₂ ≫ φ.hom₂ ≫ T'.mor₂ = 0
rw₂ : y₂ ≫ T'.mor₂ - x₂ ≫ T.mor₂ ≫ φ.hom₃ = 0
rw₃ : y₂ ≫ T'.mor₂ - x₃ ≫ φ.hom₃ = 0
rw₄ : y₂ ≫ T'.mor₂ - y₂ ≫ T'.mor₂ = 0
rw₅ rw₆ : Eq.{v + 1} (α := A ⟶ T'.obj₃) 0 0
⊢ (y₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0

Tactic:
rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, sub_self]

Premises used: CategoryTheory.Category.assoc, sub_self, CategoryTheory.Pretriangulated.TriangleMorphism.comm₂, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
refine_2 :
  ∀ (y₁ : A ⟶ T'.obj₁) (hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁),
    ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂

Tactic:
obtain ⟨y₁, hy₁⟩ := Triangle.coyoneda_exact₂ _ hT' (y₂ - x₂ ≫ φ.hom₂)
      (by rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, sub_self])

Premises used: CategoryTheory.Pretriangulated.TriangleMorphism.hom₂, CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, HSub.hSub, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
⊢ (y₁ ≫ inv φ.hom₁) ≫ φ.hom₁ = y₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
refine_2 : ∀ (x₁ : A ⟶ T.obj₁) (hx₁ : x₁ ≫ φ.hom₁ = y₁), ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂

Tactic:
obtain ⟨x₁, hx₁⟩ : ∃ (x₁ : A ⟶ T.obj₁), x₁ ≫ φ.hom₁ = y₁ := ⟨y₁ ≫ inv φ.hom₁, by simp⟩

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.Pretriangulated.TriangleMorphism.hom₁
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
x₁ : A ⟶ T.obj₁
hx₁ : x₁ ≫ φ.hom₁ = y₁
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂

Tactic:
⟨x₂ + x₁ ≫ T.mor₁, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Pretriangulated.Triangle.mor₁
-- Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
y₁ : A ⟶ T'.obj₁
hy₁ : y₂ - x₂ ≫ φ.hom₂ = y₁ ≫ T'.mor₁
x₁ : A ⟶ T.obj₁
hx₁ : x₁ ≫ φ.hom₁ = y₁
refine_2 : (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) (x₂ + x₁ ≫ T.mor₁) = y₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂

Tactic:
refine ⟨x₂ + x₁ ≫ T.mor₁, ?_⟩