awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₂)
hc₁ : Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₁) ≫ c = P.ι.map b ≫ Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₂)
hc₂ :
  Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a) =
    c ≫ Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₂)
⊢ (T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a).hom =
    (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom
have this : Eq (α :=
  P.ι.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) T₁.obj₁) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (P.ι.obj T₂.obj₁))
  (P.ι.map (Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
  (NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₁.obj₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a))
Tactic: have := P.ι.commShiftIso_hom_naturality a (1 : ℤ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
T₁ T₂ : Triangle.{v_1, u_1} P.FullSubcategory
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₁
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} P.FullSubcategory))
    (Set.preimage (β := Triangle.{v_1, u_1} C) (Functor.obj P.ι.mapTriangle)
      (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _))
    T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₁) ⟶ Triangle.obj₃ (Functor.obj P.ι.mapTriangle T₂)
hc₁ : Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₁) ≫ c = P.ι.map b ≫ Triangle.mor₂ (Functor.obj P.ι.mapTriangle T₂)
hc₂ :
  Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₁) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a) =
    c ≫ Triangle.mor₃ (Functor.obj P.ι.mapTriangle T₂)
this :
  Eq (α :=
    P.ι.obj (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor P.FullSubcategory (A := ℤ) 1) T₁.obj₁) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (P.ι.obj T₂.obj₁))
    (P.ι.map (Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a) ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
    (NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₁.obj₁ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (P.ι.map a))
⊢ (T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a).hom =
    (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom
have h : Eq (α := T₁.obj₃.obj (P := P) ⟶ (P.ι ⋙ shiftFunctor C (A := ℤ) 1).obj T₂.obj₁)
  ((T₁.mor₃ ≫ Functor.map (shiftFunctor P.FullSubcategory (A := ℤ) 1) a).hom ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
  ((P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom ≫ NatTrans.app (Iso.hom (Functor.commShiftIso P.ι 1)) T₂.obj₁)
Tactic: rw [← cancel_mono ((Functor.commShiftIso P.ι (1 : ℤ)).hom.app T₂.obj₁)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_15 : F.CommShift ℤ
inst_16 : F.IsTriangulated
inst_17 : F.Full
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _) T
X₁ : C
e₁ : F.obj X₁ ≅ T.obj₁
X₃ : C
e₃ : F.obj X₃ ≅ T.obj₃
⊢ F.essImage T.obj₂
have have : ∀ (h : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁)
  (hh :
    F.map h =
      e₃.hom ≫
        T.mor₃ ≫ Functor.map (shiftFunctor D (A := ℤ) 1) e₁.inv ≫ NatTrans.app (Iso.inv (Functor.commShiftIso F 1)) X₁),
  F.essImage T.obj₂
Tactic: have ⟨h, hh⟩ := F.map_surjective (e₃.hom ≫ T.mor₃ ≫ e₁.inv⟦1⟧' ≫
      (F.commShiftIso (1 : ℤ)).inv.app X₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D : Type u_2
inst_6 : Category.{v_2, u_2} D
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : HasZeroObject.{v_2, u_2} D
inst_9 : HasShift.{v_2, u_2, 0} D ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_11 : Pretriangulated.{v_2, u_2} D
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_15 : F.CommShift ℤ
inst_16 : F.IsTriangulated
inst_17 : F.Full
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _) T
X₁ : C
e₁ : F.obj X₁ ≅ T.obj₁
X₃ : C
e₃ : F.obj X₃ ≅ T.obj₃
h : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
hh :
  F.map h =
    e₃.hom ≫
      T.mor₃ ≫ Functor.map (shiftFunctor D (A := ℤ) 1) e₁.inv ≫ NatTrans.app (Iso.inv (Functor.commShiftIso F 1)) X₁
⊢ F.essImage T.obj₂
have obtain : ∀ (X₂ : C) (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  (H :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h)),
  F.essImage T.obj₂
Tactic: obtain ⟨X₂, f, g, H⟩ := distinguished_cocone_triangle₂ h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Subcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} 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
D_1 : Type u_2
inst_6 : Category.{v_2, u_2} D_1
inst_7 : Preadditive.{v_2, u_2} D_1
inst_8 : HasZeroObject.{v_2, u_2} D_1
inst_9 : HasShift.{v_2, u_2, 0} D_1 ℤ
inst_10 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D_1 n)
inst_11 : Pretriangulated.{v_2, u_2} D_1
E : Type u_3
inst_12 : Category.{v_3, u_3} E
inst_13 : HasShift.{v_3, u_3, 0} E ℤ
P : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
D : Type u_4
inst_15 : Category.{u_5, u_4} D
inst_16 : HasZeroObject.{u_5, u_4} D
inst_17 : Preadditive.{u_5, u_4} D
inst_18 : HasShift.{u_5, u_4, 0} D ℤ
inst_19 : ∀ (n : ℤ), Functor.Additive.{u_5, u_4, u_5, u_4} (shiftFunctor D n)
inst_20 : Pretriangulated.{u_5, u_4} D
F : Functor.{v_1, u_5, u_1, u_4} C D
inst_21 : F.CommShift ℤ
inst_22 : F.IsTriangulated
inst_23 : F.Full
⊢ (P.map F).IsTriangulated
have rw : (P.ι ⋙ F).essImage.IsTriangulated
Tactic: rw [← F.essImage_ι_comp]
-- 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 : Preadditive.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_4 : 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 Y : A
n : ℤ
f : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj X) ⟶ ι.obj Y
hn : 0 < n
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (ι.obj X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
    (Functor.map (shiftFunctor C (-n)) f) (Functor.map (shiftFunctor C (-n)) 0)
have rw : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
  (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (shiftEquiv C n) ⋙ Equivalence.inverse (shiftEquiv C n))
        (ι.obj X))
      (NatTrans.app (Iso.hom (Equivalence.unitIso (shiftEquiv C n))) (ι.obj X)) (Functor.map (shiftFunctor C (-n)) f) :
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
  (0 :
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) (ι.obj X) ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (-n)) (ι.obj Y))
Tactic: rw [← cancel_epi ((shiftEquiv C n).unitIso.hom.app _), Functor.map_zero, comp_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
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 : A
α : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K) ⟶ X₃
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
⊢ (ι ⋙ shiftFunctor C (A := ℤ) 1).map (ιK f₃ α ≫ f₁) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
have this : (Triangle.mk (ι.map f₁) f₂ f₃).mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk (ι.map f₁) f₂ f₃).mor₁ = 0
Tactic: have := comp_distTriang_mor_zero₃₁ _ 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
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₃)
Q : A
β : X₃ ⟶ ι.obj Q
inst_7 : ι.Full
inst_8 : Preadditive.{v_2, u_2} A
inst_9 : ι.Faithful
⊢ ι.map (f₁ ≫ πQ f₂ β) = ι.map 0
have this : (Triangle.mk (ι.map f₁) f₂ f₃).mor₁ ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ = 0
Tactic: have := comp_distTriang_mor_zero₁₂ _ 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
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
⊢ Mono (ιK f₃ α)
have rw : ∀ (P : A) (g : P ⟶ K), g ≫ ιK f₃ α = 0 → g = 0
Tactic: rw [mono_iff_cancel_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
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
k : B ⟶ K
hk : k ≫ ιK f₃ α = 0
⊢ k = 0
have hk₁ : (ι ⋙ shiftFunctor C (A := ℤ) 1).map (k ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
Tactic: replace hk := (ι ⋙ shiftFunctor C (1 : ℤ)).congr_map hk
Cleared hypotheses: hk
-- 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
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
k : B ⟶ K
hk : (ι ⋙ shiftFunctor C (A := ℤ) 1).map (k ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
⊢ k = 0
have a : (ι ⋙ shiftFunctor C (A := ℤ) 1).map k = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
Tactic: apply (ι ⋙ shiftFunctor C (1 : ℤ)).map_injective
-- 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
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
k : B ⟶ K
hk : (ι ⋙ shiftFunctor C (A := ℤ) 1).map (k ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
⊢ (ι ⋙ shiftFunctor C (A := ℤ) 1).map k = (ι ⋙ shiftFunctor C (A := ℤ) 1).map 0
have a : ∀ (hk : (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α) ≫ f₃ = 0),
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k)) 0
Tactic: simp only [Functor.comp_obj, Functor.comp_map, Functor.map_comp,
    shift_ι_map_ιK, Functor.map_zero, ← assoc] at hk ⊢
Cleared hypotheses: hk
-- 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
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
k : B ⟶ K
hk : (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α) ≫ f₃ = 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k)) 0
have a : ∀ (l : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂)
  (hl : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α = l ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂),
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k)) 0
Tactic: obtain ⟨l, hl⟩ := Triangle.coyoneda_exact₃ _ hT _ hk
-- 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
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
k : B ⟶ K
hk : (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α) ≫ f₃ = 0
l : Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α = l ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj B) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (ι.obj K))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k)) 0
have hl₁ : Functor.map (shiftFunctor C (A := ℤ) 1) (ι.map k) ≫ α = 0
Tactic: rw [eq_zero_of_hom_shift_pos hι l (by lia), zero_comp] at hl
Cleared hypotheses: hl