awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj 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₁) (ι.map f₂) f₃)
refine_2 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)) 0
refine_2₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) (𝟙 0)) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
have refine_2₂ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
  (Functor.map (shiftFunctor C (A := ℤ) (-1)) 0) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj 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₁) (ι.map f₂) f₃)
refine_2 :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
    (𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)) 0
refine_2₁ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) (𝟙 0)) 0
refine_2₂ :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) 0) 0
⊢ IsZero.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
have refine_2₃ : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0 ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) 0)
  0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (hypothesis)
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
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj 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₁) (ι.map f₂) f₃)
⊢ IsColimit (F := parallelPair f₁ 0) (CokernelCofork.ofπ f₂ ⋯)
have hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
  (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0)
Tactic: have hT' : Triangle.mk (0 : ((ι ⋙ shiftFunctor C (1 : ℤ)).obj 0) ⟶ _) (𝟙 (ι.obj X₃)) 0 ∈
      distTriang C := by
    refine isomorphic_distinguished _ (inv_rot_of_distTriang _
      (contractible_distinguished (ι.obj X₃))) _ ?_
    refine Triangle.isoMk _ _ (IsZero.iso ?_ ?_) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
    · dsimp
      rw [IsZero.iff_id_eq_zero, ← Functor.map_id, ← Functor.map_id, id_zero,
        Functor.map_zero, Functor.map_zero]
    · dsimp
      rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]
    all_goals simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : HasFiniteProducts.{v_2, u_2} A
inst_11 : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj 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₁) (ι.map f₂) f₃)
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
    (Triangle.mk (X := (ι ⋙ shiftFunctor C (A := ℤ) 1).obj 0) 0 (𝟙 (ι.obj X₃)) 0)
⊢ IsColimit (F := parallelPair f₁ 0) (CokernelCofork.ofπ f₂ ⋯)
have refine : Iso (C := Cocone (parallelPair f₁ 0)) (CokernelCofork.ofπ (πQ (ι.map f₂) (𝟙 (ι.obj X₃))) sorry) (CokernelCofork.ofπ f₂ sorry)
Tactic: refine IsColimit.ofIsoColimit (AbelianSubcategory.isColimitCokernelCofork hι hT hT') ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
⊢ ∃ (X₁ : A) (i : X₁ ⟶ X₂) (δ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
      (Triangle.mk (ι.map i) (ι.map π) δ)
have 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₃)),
  ∃ (X₁ : A) (i : X₁ ⟶ X₂) (δ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
      (Triangle.mk (ι.map i) (ι.map π) δ)
Tactic: obtain ⟨X₁, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map π)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (hypothesis)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
⊢ ∃ (X₁ : A) (i : X₁ ⟶ X₂) (δ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
      (Triangle.mk (ι.map i) (ι.map π) δ)
have this : admissibleMorphism ι π
Tactic: have : admissibleMorphism ι π := by simp [hA]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
⊢ ∃ (X₁ : A) (i : X₁ ⟶ X₂) (δ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
      (Triangle.mk (ι.map i) (ι.map π) δ)
have 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 α β γ)),
  ∃ (X₁ : A) (i : X₁ ⟶ X₂) (δ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
      (Triangle.mk (ι.map i) (ι.map π) δ)
Tactic: obtain ⟨K, Q, α, β, γ, hT'⟩ := this f₂ f₃ hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
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 α β γ)
⊢ Eq (α := X₃ ⟶ Q)
    (CategoryStruct.comp (Y := Cocone.pt (F := parallelPair π 0) (CokernelCofork.ofπ (πQ f₂ β) ⋯))
      (Cofork.π (CokernelCofork.ofπ (πQ f₂ β) ⋯)) (𝟙 Q))
    (CategoryStruct.comp (Y := Cocone.pt (F := parallelPair π 0) (CokernelCofork.ofπ (πQ f₂ β) ⋯))
      (Cofork.π (CokernelCofork.ofπ (πQ f₂ β) ⋯)) 0)
have dsimp : πQ f₂ β ≫ 𝟙 Q = πQ f₂ β ≫ 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
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 α β γ)
⊢ πQ f₂ β ≫ 𝟙 Q = πQ f₂ β ≫ 0
have rw : πQ f₂ β = πQ f₂ β ≫ 0
Tactic: rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
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 α β γ)
rw : πQ f₂ β = πQ f₂ β ≫ 0
⊢ πQ f₂ β ≫ 𝟙 Q = πQ f₂ β ≫ 0
have rw₁ : πQ f₂ β = 0
Tactic: rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
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 α β γ)
rw : πQ f₂ β = πQ f₂ β ≫ 0
rw₁ : πQ f₂ β = 0
⊢ πQ f₂ β ≫ 𝟙 Q = πQ f₂ β ≫ 0
have rw₂ : π ≫ πQ f₂ β = π ≫ 0
Tactic: rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
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 α β γ)
rw : πQ f₂ β = πQ f₂ β ≫ 0
rw₁ : πQ f₂ β = 0
rw₂ : π ≫ πQ f₂ β = π ≫ 0
⊢ πQ f₂ β ≫ 𝟙 Q = πQ f₂ β ≫ 0
have rw₃ : π ≫ πQ f₂ β = 0
Tactic: rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (goal)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
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 α β γ)
rw : πQ f₂ β = πQ f₂ β ≫ 0
rw₁ : πQ f₂ β = 0
rw₂ : π ≫ πQ f₂ β = π ≫ 0
rw₃ : π ≫ πQ f₂ β = 0
⊢ πQ f₂ β ≫ 𝟙 Q = πQ f₂ β ≫ 0
have rw₄ : Eq.{v_2 + 1} (α := X₂ ⟶ Q) 0 0
Tactic: rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory (hypothesis)
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
inst_10 : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst_11 : Epi π
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₃)
this : admissibleMorphism ι π
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 α β γ)
⊢ ∃ (X₁ : A) (i : X₁ ⟶ X₂) (δ : ι.obj X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj X₁)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_2 inst_4 _)
      (Triangle.mk (ι.map i) (ι.map π) δ)
have hQ : Eq.{v_2 + 1} (α := Q ⟶ Q) (𝟙 Q) 0
Tactic: have hQ : 𝟙 Q = 0 :=
    Cofork.IsColimit.hom_ext (isColimitCokernelCofork hι hT hT') (by
      dsimp
      rw [comp_id, comp_zero, ← cancel_epi π, comp_zero, mor₁_πQ hT β])