awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
M : Type u_1
inst_2 : AddGroup M
inst_3 : HasShift.{v, u, u_1} C M
inst_4 : HasZeroMorphisms.{v, u} C
inst_5 : P.IsStableUnderShift M
n : M
X : C
hX : P.leftOrthogonal X
Y : C
f : Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y
hY : P Y
obtain :
  ∀ (g : X ⟶ Functor.obj.{v, v, u, u} (Equivalence.inverse (shiftEquiv C n)) Y),
    Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y)
      ((Equiv.symm (Adjunction.homEquiv (Equivalence.toAdjunction (shiftEquiv C n)) X Y) :
            (a : X ⟶ (shiftEquiv C n).inverse.obj Y) → (shiftEquiv C n).functor.obj X ⟶ Y)
          g :
        Functor.obj.{v, v, u, u} (Equivalence.functor (shiftEquiv C n)) X ⟶ Y)
      (0 : Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y)
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := ((shiftEquiv C n).toAdjunction.homEquiv _ _).symm.surjective f

Premises used: CategoryTheory.shiftEquiv, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.homEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
M : Type u_1
inst_2 : AddGroup M
inst_3 : HasShift.{v, u, u_1} C M
inst_4 : HasZeroMorphisms.{v, u} C
inst_5 : P.IsStableUnderShift M
n : M
X : C
hX : P.leftOrthogonal X
Y : C
hY : P Y
g : X ⟶ Functor.obj.{v, v, u, u} (Equivalence.inverse (shiftEquiv C n)) Y
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y)
    ((Equiv.symm (Adjunction.homEquiv (Equivalence.toAdjunction (shiftEquiv C n)) X Y) :
          (a : X ⟶ (shiftEquiv C n).inverse.obj Y) → (shiftEquiv C n).functor.obj X ⟶ Y)
        g :
      Functor.obj.{v, v, u, u} (Equivalence.functor (shiftEquiv C n)) X ⟶ Y)
    (0 : Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y)

Tactic:
simp [hX g (P.le_shift (-n) _ hY), Adjunction.homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_counit, Neg.neg, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _) T
h₁ : P.rightOrthogonal T.obj₁
h₃ : P.rightOrthogonal T.obj₃
X : C
f : X ⟶ T.obj₂
hX : P X
obtain : ∀ (g : X ⟶ T.obj₁), g ≫ T.mor₁ = 0
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := Pretriangulated.Triangle.coyoneda_exact₂ T hT f (h₃ _ hX)

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _) T
h₁ : P.rightOrthogonal T.obj₁
h₃ : P.rightOrthogonal T.obj₃
X : C
hX : P X
g : X ⟶ T.obj₁
⊢ g ≫ T.mor₁ = 0

Tactic:
simp [h₁ g hX]
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _) T
h₁ : P.leftOrthogonal T.obj₁
h₃ : P.leftOrthogonal T.obj₃
Y : C
f : T.obj₂ ⟶ Y
hY : P Y
obtain : ∀ (g : T.obj₃ ⟶ Y), T.mor₂ ≫ g = 0
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := Pretriangulated.Triangle.yoneda_exact₂ T hT f (h₁ _ hY)

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _) T
h₁ : P.leftOrthogonal T.obj₁
h₃ : P.leftOrthogonal T.obj₃
Y : C
hY : P Y
g : T.obj₃ ⟶ Y
⊢ T.mor₂ ≫ g = 0

Tactic:
simp [h₃ g hY]
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
⊢ P.rightOrthogonal.IsTriangulated

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
⊢ P.leftOrthogonal.IsTriangulated

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
h : ∀ (Y : C), P.trW.isLocal Y ↔ P.rightOrthogonal Y
⊢ P.trW.isLocal = P.rightOrthogonal

Tactic:
ext Y
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
⊢ P.trW.isLocal Y ↔ P.rightOrthogonal Y

Tactic:
⟨fun hY X f hX ↦ ?_, fun hY X₁ X₂ f ⟨X₃, g, h, hT, hX₃⟩ ↦ ⟨?_, fun α ↦ ?_⟩⟩

Premises used: And.intro, Iff.intro, CategoryTheory.CategoryStruct.comp, Function.Bijective, _private.0.CategoryTheory.ObjectProperty.isLocal_trW.match_1
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
h : ∀ (hY : P.trW.isLocal Y) (X : C) (f : X ⟶ Y) (hX : P X), f = 0
h₁ :
  ∀ (hY : P.rightOrthogonal Y) (X₁ X₂ : C) (f : X₁ ⟶ X₂),
    P.trW f →
      ∀ (X₃ : C) (g : X₂ ⟶ X₃) (h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁)
        (hT :
          Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
            (Triangle.mk f g h))
        (hX₃ : P X₃), Function.Injective (β := X₁ ⟶ Y) fun (g : X₂ ⟶ Y) ↦ f ≫ g
h₂ :
  ∀ (hY : P.rightOrthogonal Y) (X₁ X₂ : C) (f : X₁ ⟶ X₂),
    P.trW f →
      ∀ (X₃ : C) (g : X₂ ⟶ X₃) (h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁)
        (hT :
          Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
            (Triangle.mk f g h))
        (hX₃ : P X₃) (α : X₁ ⟶ Y), ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = α
⊢ P.trW.isLocal Y ↔ P.rightOrthogonal Y

Tactic:
refine ⟨fun hY X f hX ↦ ?_, fun hY X₁ X₂ f ⟨X₃, g, h, hT, hX₃⟩ ↦ ⟨?_, fun α ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.trW.isLocal Y
X : C
f : X ⟶ Y
hX : P X
⊢ Eq.{v + 1} (α := Triangle.obj₁.{v, u} (Triangle.mk (X := 0) 0 (𝟙 X) 0) ⟶ Y)
    (Triangle.mor₁ (Triangle.mk (X := 0) 0 (𝟙 X) 0) ≫ f) (Triangle.mor₁ (Triangle.mk (X := 0) 0 (𝟙 X) 0) ≫ 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.trW.isLocal Y
X : C
f : X ⟶ Y
hX : P X
⊢ f = 0

Tactic:
exact (hY _ (trW.mk P (contractible_distinguished₁ X) hX)).injective (by simp)

Premises used: Function.Bijective.injective, CategoryTheory.ObjectProperty.trW.mk, CategoryTheory.Pretriangulated.contractible_distinguished₁
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
this : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
α₁ α₂ : X₂ ⟶ Y
hα : Eq.{v + 1} (α := X₁ ⟶ Y) ((fun (g : X₂ ⟶ Y) ↦ f ≫ g) α₁) ((fun (g : X₂ ⟶ Y) ↦ f ≫ g) α₂)
⊢ f ≫ (α₁ - α₂) = 0

Tactic:
simpa [sub_eq_zero] using hα

Premises used: sub_eq_zero
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
this : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
α₁ α₂ : X₂ ⟶ Y
hα : Eq.{v + 1} (α := X₁ ⟶ Y) ((fun (g : X₂ ⟶ Y) ↦ f ≫ g) α₁) ((fun (g : X₂ ⟶ Y) ↦ f ≫ g) α₂)
⊢ α₁ = α₂

Tactic:
simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero] using hα)

Premises used: sub_eq_zero, HSub.hSub
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
h₁ : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
⊢ Function.Injective (β := X₁ ⟶ Y) fun (g : X₂ ⟶ Y) ↦ f ≫ g

Tactic:
suffices ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0 from fun α₁ α₂ hα ↦ by
      simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero] using hα)
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
α : X₂ ⟶ Y
hα : f ≫ α = 0
h₁ : ∀ (β : (Triangle.mk f g h).obj₃ ⟶ Y) (hα : f ≫ (Triangle.mk f g h).mor₂ ≫ β = 0), (Triangle.mk f g h).mor₂ ≫ β = 0
⊢ α = 0

Tactic:
obtain ⟨β, rfl⟩ := Triangle.yoneda_exact₂ _ hT α hα

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
β : (Triangle.mk f g h).obj₃ ⟶ Y
hα : f ≫ (Triangle.mk f g h).mor₂ ≫ β = 0
⊢ (Triangle.mk f g h).mor₂ ≫ β = 0

Tactic:
simp [hY β hX₃]
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
α : X₁ ⟶ Y
h₁ :
  ∀ (β : (Triangle.mk f g h).invRotate.obj₃ ⟶ Y),
    ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = (Triangle.mk f g h).invRotate.mor₂ ≫ β
⊢ ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = α

Tactic:
obtain ⟨β, rfl⟩ := Triangle.yoneda_exact₂ _ (inv_rot_of_distTriang _ hT)
      α (hY _ (P.le_shift _ _ hX₃))

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, CategoryTheory.Pretriangulated.inv_rot_of_distTriang, rfl, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
β : (Triangle.mk f g h).invRotate.obj₃ ⟶ Y
⊢ ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = (Triangle.mk f g h).invRotate.mor₂ ≫ β

Tactic:
⟨β, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
β : (Triangle.mk f g h).invRotate.obj₃ ⟶ Y
⊢ ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = (Triangle.mk f g h).invRotate.mor₂ ≫ β

Tactic:
exact ⟨β, rfl⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
h : ∀ (X : C), P.trW.isColocal X ↔ P.leftOrthogonal X
⊢ P.trW.isColocal = P.leftOrthogonal

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
⊢ P.trW.isColocal X ↔ P.leftOrthogonal X

Tactic:
⟨fun hX Y f hY ↦ ?_, fun hX Y₂ Y₃ h hh ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
h : ∀ (hX : P.trW.isColocal X) (Y : C) (f : X ⟶ Y) (hY : P Y), f = 0
h₁ :
  ∀ (hX : P.leftOrthogonal X) (Y₂ Y₃ : C) (h : Y₂ ⟶ Y₃) (hh : P.trW h),
    Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
⊢ P.trW.isColocal X ↔ P.leftOrthogonal X

Tactic:
refine ⟨fun hX Y f hY ↦ ?_, fun hX Y₂ Y₃ h hh ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.trW.isColocal X
Y : C
f : X ⟶ Y
hY : P Y
⊢ f ≫ (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y))).mor₁ =
    0 ≫ (Triangle.mk (Y := 0) 0 0 (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y))).mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.trW.isColocal X
Y : C
f : X ⟶ Y
hY : P Y
⊢ f = 0

Tactic:
exact (hX _ (trW.mk P (contractible_distinguished₂ Y) (P.le_shift _ _ hY))).injective (by simp)

Premises used: CategoryTheory.Pretriangulated.contractible_distinguished₂, Function.Bijective.injective, CategoryTheory.ObjectProperty.trW.mk, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh : P.trW h
⊢ ∃ (X : C) (f : X ⟶ Y₂) (h_1 : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f h h_1)),
    P X

Tactic:
rw [trW_iff'] at hh

Premises used: CategoryTheory.ObjectProperty.trW_iff'
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh :
  ∃ (X : C) (f : X ⟶ Y₂) (h_1 : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f h h_1)),
    P X
h₁ :
  ∀ (Y₁ : C) (f : Y₁ ⟶ Y₂) (g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁)
    (hT :
      Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
        (Triangle.mk f h g))
    (hY₁ : P Y₁), Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
⊢ Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h

Tactic:
obtain ⟨Y₁, f, g, hT, hY₁⟩ := hh
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
⊢ Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h

Tactic:
⟨?_, fun α ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
h₁ : Function.Injective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
h₂ : ∀ (α : X ⟶ Y₃), ∃ (a : X ⟶ Y₂), (fun (f : X ⟶ Y₂) ↦ f ≫ h) a = α
⊢ Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h

Tactic:
refine ⟨?_, fun α ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{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)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
this : ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0
α₁ α₂ : X ⟶ Y₂
hα : Eq.{v + 1} (α := X ⟶ Y₃) ((fun (f : X ⟶ Y₂) ↦ f ≫ h) α₁) ((fun (f : X ⟶ Y₂) ↦ f ≫ h) α₂)
⊢ (α₁ - α₂) ≫ h = 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero