awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsStableUnderShift ℤ
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : P.trW f
n : ℤ
⊢ P.trW (X := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₁) (Functor.map (shiftFunctor C n) f)
have rw : P.trW
  (HSMul.hSMul (β :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₂)
    n.negOnePow (Functor.map (shiftFunctor C n) f))
Tactic: rw [← smul_mem_trW_iff _ _ (n.negOnePow)]
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsStableUnderShift ℤ
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : P.trW f
n : ℤ
⊢ P.trW
    (HSMul.hSMul (β :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₂)
      n.negOnePow (Functor.map (shiftFunctor C n) f))
have obtain : ∀ (X₃ : C) (g : X₂ ⟶ X₃) (h : X₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁)
  (hT :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h))
  (mem : P X₃),
  P.trW
    (HSMul.hSMul (β :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₁ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X₂)
      n.negOnePow (Functor.map (shiftFunctor C n) f))
Tactic: obtain ⟨X₃, g, h, hT, mem⟩ := hf
Cleared hypotheses: hf
-- 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.IsStableUnderShift ℤ
n : ℤ
⊢ P.trW.inverseImage (shiftFunctor C n) = P.trW
have h : ∀ ⦃K L : C⦄ (f : K ⟶ L), P.trW.inverseImage (shiftFunctor C n) f ↔ P.trW f
Tactic: ext K L f
-- 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 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P.trW f → P.trW g → P.trW (f ≫ g)
have rw : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P.isoClosure.trW f → P.isoClosure.trW g → P.isoClosure.trW (f ≫ g)
Tactic: rw [← trW_isoClosure]
-- 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 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X₁ X₂ X₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
Z₁₂ : C
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁
H₁₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₁₂ v₁₂ w₁₂)
mem₁₂ : P.isoClosure Z₁₂
Z₂₃ : C
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₂
H₂₃ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk u₂₃ v₂₃ w₂₃)
mem₂₃ : P.isoClosure Z₂₃
⊢ P.isoClosure.trW (u₁₂ ≫ u₂₃)
have obtain : ∀ (Z₁₃ : C) (v₁₃ : X₃ ⟶ Z₁₃) (w₁₂ : Z₁₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X₁)
  (H₁₃ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk (u₁₂ ≫ u₂₃) v₁₃ w₁₂)),
  P.isoClosure.trW (u₁₂ ≫ u₂₃)
Tactic: obtain ⟨Z₁₃, v₁₃, w₁₂, H₁₃⟩ := distinguished_cocone_triangle (u₁₂ ≫ u₂₃)
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
⊢ P.trW T.mor₁ ↔ P T.obj₃
have mp : P.trW T.mor₁ → P T.obj₃
Tactic: constructor
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
mp : P.trW T.mor₁ → P T.obj₃
⊢ P.trW T.mor₁ ↔ P T.obj₃
have mpr : P T.obj₃ → P.trW T.mor₁
Tactic: constructor
-- 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
P : ObjectProperty.{v_1, u_1} C
inst_6 : P.IsClosedUnderIsomorphisms
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
Z : C
g : T.obj₂ ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) T.obj₁
hT' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk T.mor₁ g h)
mem : P Z
⊢ P T.obj₃
have mp : ∀ (e : Triangle.mk T.mor₁ g h ≅ T),
  e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁))) ∧
      e.hom.hom₂ = Arrow.Hom.right (Iso.hom (Iso.refl (Arrow.mk (Triangle.mk T.mor₁ g h).mor₁))) →
    P T.obj₃
Tactic: obtain ⟨e, _⟩ := exists_iso_of_arrow_iso _ _ hT' hT (Iso.refl _)
-- 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
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
have obtain : ∀ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X)
  (hT :
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
      (Triangle.mk s g h)),
  (P.inverseImage F).trW s ↔ P.trW (F.map s)
Tactic: obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle s
-- 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
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
have eq₁ : (P.inverseImage F).trW (Triangle.mk s g h).mor₁ ↔ P.inverseImage F (Triangle.mk s g h).obj₃
Tactic: have eq₁ := (P.inverseImage F).trW_iff_of_distinguished _ hT
-- 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
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
eq₁ : (P.inverseImage F).trW (Triangle.mk s g h).mor₁ ↔ P.inverseImage F (Triangle.mk s g h).obj₃
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
have eq₂ : P.trW (X := Triangle.obj₁ (Functor.obj F.mapTriangle (Triangle.mk s g h)))
    (Triangle.mor₁ (Functor.obj F.mapTriangle (Triangle.mk s g h))) ↔
  P (Triangle.obj₃ (Functor.obj F.mapTriangle (Triangle.mk s g h)))
Tactic: have eq₂ := P.trW_iff_of_distinguished _ (F.map_distinguished _ hT)
-- 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
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
have rw : P.inverseImage F Z ↔ P.trW (F.map s)
Tactic: rw [eq₁, prop_inverseImage_iff, eq₂]
-- 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
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
rw : P.inverseImage F Z ↔ P.trW (F.map s)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
have rw₁ : P (F.obj Z) ↔ P.trW (F.map s)
Tactic: rw [eq₁, prop_inverseImage_iff, eq₂]
-- 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
P : ObjectProperty.{v_1, u_1} C
F : Functor.{v_2, v_1, u_2, u_1} D C
inst_12 : F.CommShift ℤ
inst_13 : F.IsTriangulated
inst_14 : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_8 _ inst_7 inst_10 _)
    (Triangle.mk s g h)
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
rw : P.inverseImage F Z ↔ P.trW (F.map s)
rw₁ : P (F.obj Z) ↔ P.trW (F.map s)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)
have rw₂ : P (F.obj Z) ↔ P (F.obj Z)
Tactic: rw [eq₁, prop_inverseImage_iff, eq₂]
-- 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 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.RightFraction X Y
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
have obtain : ∀ (Z : C) (f : X ⟶ Z) (g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW)))
  (H :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk (φ.s (W := P.trW)) f g))
  (mem : P Z), ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
Tactic: obtain ⟨Z, f, g, H, mem⟩ := φ.hs
-- 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 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW))
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (φ.s (W := P.trW)) f g)
mem : P Z
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
have obtain : ∀ (Y' : C) (s' : Y ⟶ Y') (f' : Y' ⟶ Z)
  (mem' :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW))))),
  ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
Tactic: obtain ⟨Y', s', f', mem'⟩ := distinguished_cocone_triangle₂ (g ≫ φ.f⟦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 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X Y : C
φ : P.trW.RightFraction X Y
Z : C
f : X ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (φ.X' (W := P.trW))
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk (φ.s (W := P.trW)) f g)
mem : P Z
Y' : C
s' : Y ⟶ Y'
f' : Y' ⟶ Z
mem' :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW))))
⊢ ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
have obtain : ∀
  (b :
    (Triangle.mk (φ.s (W := P.trW)) f g).obj₂ ⟶
      (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).obj₂)
  (hb₁ :
    (Triangle.mk (φ.s (W := P.trW)) f g).mor₁ ≫ b =
      φ.f (W := P.trW) ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₁),
  (Triangle.mk (φ.s (W := P.trW)) f g).mor₂ ≫ 𝟙 Z =
      b ≫ (Triangle.mk s' f' (g ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (φ.f (W := P.trW)))).mor₂ →
    ∃ (ψ : P.trW.LeftFraction X Y), φ.f (W := P.trW) ≫ ψ.s (W := P.trW) = φ.s (W := P.trW) ≫ ψ.f (W := P.trW)
Tactic: obtain ⟨b, ⟨hb₁, _⟩⟩ :=
      complete_distinguished_triangle_morphism₂ _ _ H mem' φ.f (𝟙 Z) (by simp)
-- 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 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s g h)
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
⊢ s ≫ (f₁ - f₂) = 0
have rw : s ≫ f₁ - s ≫ f₂ = 0
Tactic: rw [comp_sub, hf₁, sub_self]
-- 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 : IsTriangulated.{v_1, u_1} C
inst_15 : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X'
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk s g h)
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
rw : s ≫ f₁ - s ≫ f₂ = 0
⊢ s ≫ (f₁ - f₂) = 0
have rw₁ : s ≫ f₂ - s ≫ f₂ = 0
Tactic: rw [comp_sub, hf₁, sub_self]