awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
W' : A
x₁ : W' ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
m : W' ⟶ K
hm : m ≫ ιK f₃ α = x₁
this : Mono (ιK f₃ α)
rw : m ≫ ιK f₃ α = Exists.choose (p := fun (k : W' ⟶ K) ↦ k ≫ ιK f₃ α = x₁) ⋯ ≫ ιK f₃ α
rw₁ : m ≫ ιK f₃ α = x₁
rw₂ rw₃ : x₁ = x₁
⊢ m = Exists.choose (p := fun (k : W' ⟶ K) ↦ k ≫ ιK f₃ α = x₁) ⋯

Tactic:
rw [← cancel_mono (ιK f₃ α), (exists_lift_ιK hι hT hT' x₁ hx₁).choose_spec, hm]

Premises used: Exists.choose_spec, CategoryTheory.Triangulated.AbelianSubcategory.exists_lift_ιK, CategoryTheory.Triangulated.AbelianSubcategory.ιK, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
⊢ (Triangle.mk (ι.map f₁) f₂ f₃).mor₁ ≫ ι.map x₂ = 0

Tactic:
simp [← ι.map_comp, hx₂]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
obtain :
  ∀ (x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B) (hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁),
    ∃ (k : Q ⟶ B), πQ f₂ β ≫ k = x₂
⊢ ∃ (k : Q ⟶ B), πQ f₂ β ≫ k = x₂

Tactic:
obtain ⟨x₁, hx₁⟩ := Triangle.yoneda_exact₂ _ hT (ι.map x₂) (by simp [← ι.map_comp, hx₂])

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
⊢ LT.lt (α := ℤ) 0 1

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
obtain :
  ∀ (k : (Triangle.mk α β γ).obj₃ ⟶ ι.obj B) (hk : x₁ = (Triangle.mk α β γ).mor₂ ≫ k), ∃ (k : Q ⟶ B), πQ f₂ β ≫ k = x₂
⊢ ∃ (k : Q ⟶ B), πQ f₂ β ≫ k = x₂

Tactic:
obtain ⟨k, hk⟩ := Triangle.yoneda_exact₂ _ hT' x₁
    (eq_zero_of_hom_shift_pos hι _ (by lia))

Premises used: CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂, CategoryTheory.Triangulated.AbelianSubcategory.eq_zero_of_hom_shift_pos
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
k : (Triangle.mk α β γ).obj₃ ⟶ ι.obj B
hk : x₁ = (Triangle.mk α β γ).mor₂ ≫ k
⊢ ∃ (k : Q ⟶ B), πQ f₂ β ≫ k = x₂

Tactic:
exact ⟨ι.preimage k, ι.map_injective (by cat_disch)⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
Z' : A
x₂ : X₂ ⟶ Z'
hx₂ : f₁ ≫ x₂ = 0
m : Q ⟶ Z'
hm : πQ f₂ β ≫ m = x₂
⊢ Epi (πQ f₂ β)

Tactic:
have := epi_πQ hι hT hT'
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
Z' : A
x₂ : X₂ ⟶ Z'
hx₂ : f₁ ≫ x₂ = 0
m : Q ⟶ Z'
hm : πQ f₂ β ≫ m = x₂
this : Epi (πQ f₂ β)
rw : πQ f₂ β ≫ m = πQ f₂ β ≫ Exists.choose (p := fun (k : Q ⟶ Z') ↦ πQ f₂ β ≫ k = x₂) ⋯
rw₁ : πQ f₂ β ≫ m = x₂
rw₂ rw₃ : x₂ = x₂
⊢ m = Exists.choose (p := fun (k : Q ⟶ Z') ↦ πQ f₂ β ≫ k = x₂) ⋯

Tactic:
rw [← cancel_epi (πQ f₂ β), (exists_desc_πQ hι hT hT' x₂ hx₂).choose_spec, hm]

Premises used: Exists.choose_spec, CategoryTheory.Triangulated.AbelianSubcategory.πQ, CategoryTheory.Triangulated.AbelianSubcategory.exists_desc_πQ, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
⊢ HasKernel f₁

Tactic:
⟨_, isLimitKernelFork hι hT hT'⟩

Premises used: CategoryTheory.Triangulated.AbelianSubcategory.isLimitKernelFork, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
⊢ HasCokernel f₁

Tactic:
⟨_, isColimitCokernelCofork hι hT hT'⟩

Premises used: CategoryTheory.Triangulated.AbelianSubcategory.isColimitCokernelCofork, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
obtain :
  ∀ (X₃ : C) (f₂ : ι.obj X₂ ⟶ X₃) (f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁))
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
        (Triangle.mk (ι.map f₁) f₂ f₃)),
    HasKernel f₁
⊢ HasKernel f₁

Tactic:
obtain ⟨X₃, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map f₁)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
obtain :
  ∀ (K Q : A) (α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃) (β : X₃ ⟶ ι.obj Q)
    (γ :
      ι.obj Q ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)))
    (hT' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
        (Triangle.mk α β γ)),
    HasKernel f₁
⊢ HasKernel f₁

Tactic:
obtain ⟨K, Q, α, β, γ, hT'⟩ := hf₁ f₂ f₃ hT
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
⊢ HasKernel f₁

Tactic:
hasKernel hι hT hT'

Premises used: CategoryTheory.Triangulated.AbelianSubcategory.hasKernel
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
K Q : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ :
  ι.obj Q ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk α β γ)
⊢ HasKernel f₁

Tactic:
exact hasKernel hι hT hT'

Premises used: CategoryTheory.Triangulated.AbelianSubcategory.hasKernel
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
obtain :
  ∀ (X₃ : C) (f₂ : ι.obj X₂ ⟶ X₃) (f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁))
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
        (Triangle.mk (ι.map f₁) f₂ f₃)),
    HasCokernel f₁
⊢ HasCokernel f₁

Tactic:
obtain ⟨X₃, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map f₁)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
Goal:
C : Type u_1
A : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : Category.{v_2, u_2} A
ι : Functor.{v_2, v_1, u_2, u_1} A C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj Y)), n < 0 → f = 0
inst_7 : Preadditive.{v_2, u_2} A
inst_8 : ι.Full
inst_9 : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (ι.map f₁) f₂ f₃)
obtain :
  ∀ (K Q : A) (α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃) (β : X₃ ⟶ ι.obj Q)
    (γ :
      ι.obj Q ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K)))
    (hT' :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
        (Triangle.mk α β γ)),
    HasCokernel f₁
⊢ HasCokernel f₁

Tactic:
obtain ⟨K, Q, α, β, γ, hT'⟩ := hf₁ f₂ f₃ hT