awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι_1
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
F : Functor.{v_1, v_3, u_1, u_3} C D
inst_13 : F.CommShift ℤ
inst_14 : F.IsTriangulated
ι : Type u_4
inst_15 : Category.{v_4, u_4} ι
X Y : Triangulated.SpectralObject.{v_1, u_1, v_4, u_4} C ι
α : X ⟶ Y
i j k : ι
f : i ⟶ j
g : j ⟶ k
hf :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ f))) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
rw :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (X.δ f g) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
        map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
⊢ Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    ((F.map (X.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f))) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
have rw₁ : Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
  (F.map (X.δ f g) ≫
    F.map (map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
  (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
Tactic: rw [Category.assoc, ← hf, ← F.map_comp_assoc, α.comm, F.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.SpectralObject (goal)
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι_1
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
D : Type u_3
inst_7 : Category.{v_3, u_3} D
inst_8 : HasZeroObject.{v_3, u_3} D
inst_9 : HasShift.{v_3, u_3, 0} D ℤ
inst_10 : Preadditive.{v_3, u_3} D
inst_11 : ∀ (n : ℤ), Additive.{v_3, u_3, v_3, u_3} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_3, u_3} D
F : Functor.{v_1, v_3, u_1, u_3} C D
inst_13 : F.CommShift ℤ
inst_14 : F.IsTriangulated
ι : Type u_4
inst_15 : Category.{v_4, u_4} ι
X Y : Triangulated.SpectralObject.{v_1, u_1, v_4, u_4} C ι
α : X ⟶ Y
i j k : ι
f : i ⟶ j
g : j ⟶ k
hf :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (X.ω₁.obj (mk₁ f))) ⟶
      obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
rw :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (X.δ f g) ≫
      NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f)) ≫
        map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
rw₁ :
  Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    (F.map (X.δ f g) ≫
      F.map (map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
        NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
⊢ Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
    ((F.map (X.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (X.ω₁.obj (mk₁ f))) ≫
      map (shiftFunctor D (A := ℤ) 1) (F.map (α.hom.app (mk₁ f))))
    (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
have rw₂ : Eq (α := F.obj (X.ω₁.obj (mk₁ g)) ⟶ obj.{v_3, v_3, u_3, u_3} (shiftFunctor D (A := ℤ) 1) (F.obj (Y.ω₁.obj (mk₁ f))))
  (F.map (X.δ f g ≫ map (shiftFunctor C (A := ℤ) 1) (α.hom.app (mk₁ f))) ≫
    NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
  (F.map (α.hom.app (mk₁ g)) ≫ F.map (Y.δ f g) ≫ NatTrans.app (Iso.hom (commShiftIso F 1)) (Y.ω₁.obj (mk₁ f)))
Tactic: rw [Category.assoc, ← hf, ← F.map_comp_assoc, α.comm, F.map_comp_assoc]
-- 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.IsTriangulatedClosed₃
X Y : C
a : X ⟶ Y
hX : P X
hY : P Y
⊢ ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
have obtain : ∀ (Z : C) (b : Y ⟶ Z) (c : 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 a b c)),
  ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
Tactic: obtain ⟨Z, b, c, h⟩ := distinguished_cocone_triangle a
-- 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.IsTriangulatedClosed₃
X Y : C
a : X ⟶ Y
hX : P X
hY : P Y
Z : C
b : Y ⟶ Z
c : 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 a b c)
⊢ ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
have obtain : ∀ (Z' : C) (hZ' : P Z') (e : (Triangle.mk a b c).obj₃ ≅ Z'),
  ∃ (Z : C) (_ : P Z) (b : Y ⟶ Z) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
Tactic: obtain ⟨Z', hZ', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₃' _ h hX hY
-- 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.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
⊢ ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
have obtain : ∀ (X : C) (a : X ⟶ Y) (c : 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 a b c)),
  ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
Tactic: obtain ⟨X, a, c, h⟩ := distinguished_cocone_triangle₁ b
-- 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.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : 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 a b c)
⊢ ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
have obtain : ∀ (X' : C) (hX' : P X') (e : (Triangle.mk a b c).obj₁ ≅ X'),
  ∃ (X : C) (_ : P X) (a : X ⟶ Y) (c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
Tactic: obtain ⟨X', hX', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₁' _ h hY hZ
-- 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.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hX : P X
hZ : P Z
⊢ ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
have obtain : ∀ (Y : C) (a : X ⟶ Y) (b : Y ⟶ Z)
  (h :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)),
  ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
Tactic: obtain ⟨Y, a, b, h⟩ := distinguished_cocone_triangle₂ c
-- 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.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk a b c)
⊢ ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
have obtain : ∀ (Y' : C) (hY' : P Y') (e : (Triangle.mk a b c).obj₂ ≅ Y'),
  ∃ (Y : C) (_ : P Y) (a : X ⟶ Y) (b : Y ⟶ Z),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk a b c)
Tactic: obtain ⟨Y', hY', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' _ h hX hZ
-- 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.IsTriangulatedClosed₂
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
X₁ : C
h₁ : P X₁
e₁ : T.obj₁ ≅ X₁
X₃ : C
h₃ : P X₃
e₃ : T.obj₃ ≅ X₃
⊢ (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom)
          (e₃.inv ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom)).mor₃ ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) e₁.symm.hom =
    e₃.symm.hom ≫ T.mor₃
have dsimp : (e₃.inv ≫ T.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.inv =
  e₃.inv ≫ T.mor₃
Tactic: dsimp
-- 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 Q : ObjectProperty.{v_1, u_1} C
inst_14 : P.IsTriangulated
inst_15 : Q.IsTriangulated
inst_16 : Q.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
h₁ : (P ⊓ Q) T.obj₁
h₃ : (P ⊓ Q) T.obj₃
⊢ (P ⊓ Q).isoClosure T.obj₂
have obtain : ∀ (Y : C) (hY : P Y) (e : T.obj₂ ≅ Y), (P ⊓ Q).isoClosure T.obj₂
Tactic: obtain ⟨Y, hY, ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₂' T hT h₁.1 h₃.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 Q R : ObjectProperty.{v_1, u_1} C
inst_14 : P.Nonempty
inst_15 : Q.Nonempty
⊢ (P.extensionProduct Q).Nonempty
have obtain : ∀ (Y : C) (f : P.arbitrary ⟶ Y) (g : Y ⟶ Q.arbitrary)
  (hT :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g 0)),
  (P.extensionProduct Q).Nonempty
Tactic: obtain ⟨Y, f, g, hT⟩ := distinguished_cocone_triangle₂ (0 : Q.arbitrary ⟶ P.arbitrary⟦(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
P : ObjectProperty.{v_1, u_1} C
⊢ extensionProduct ⊥ P = ⊥
have rw : extensionProduct ⊥ P ≤ ⊥
Tactic: rw [eq_bot_iff]
-- 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
i : C
⊢ extensionProduct ⊥ P i ≤ ⊥ i
have this : ∀ (w w_1 : C) (w_2 : w ⟶ i) (w_3 : i ⟶ w_1)
  (w_4 : w_1 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) w),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk w_2 w_3 w_4) →
    ∀ (h : ⊥ w), P w_1 → ⊥ i
Tactic: ⟨_, _, _, _, _, _, 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
P : ObjectProperty.{v_1, u_1} C
⊢ P.extensionProduct ⊥ = ⊥
have rw : P.extensionProduct ⊥ ≤ ⊥
Tactic: rw [eq_bot_iff]
-- 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
i : C
⊢ P.extensionProduct ⊥ i ≤ ⊥ i
have this : ∀ (w w_1 : C) (w_2 : w ⟶ i) (w_3 : i ⟶ w_1)
  (w_4 : w_1 ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) w),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk w_2 w_3 w_4) →
    P w → ∀ (h : ⊥ w_1), ⊥ i
Tactic: ⟨_, _, _, _, _, _, _, 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
P Q P' : ObjectProperty.{v_1, u_1} C
h : P ≤ P'
X : C
⊢ P.extensionProduct Q X ≤ P'.extensionProduct Q X
have this : ∀ (Y Z : C) (f : Y ⟶ X) (g : X ⟶ Z) (k : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y)
  (hT :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g k))
  (hP : P Y) (hQ : Q Z), P'.extensionProduct Q X
Tactic: ⟨Y, Z, f, g, k, hT, hP, hQ⟩
-- 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 Q Q' : ObjectProperty.{v_1, u_1} C
h : Q ≤ Q'
X : C
⊢ P.extensionProduct Q X ≤ P.extensionProduct Q' X
have this : ∀ (Y Z : C) (f : Y ⟶ X) (g : X ⟶ Z) (k : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y)
  (hT :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g k))
  (hP : P Y) (hQ : Q Z), P.extensionProduct Q' X
Tactic: ⟨Y, Z, f, g, k, hT, hP, hQ⟩
-- 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 Q R : ObjectProperty.{v_1, u_1} C
X X' : C
i : X ≅ X'
⊢ P.extensionProduct Q X → P.extensionProduct Q X'
have this : ∀ (Y Z : C) (f : Y ⟶ X) (g : X ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y)
  (hT :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f g h))
  (hP : P Y) (hQ : Q Z), P.extensionProduct Q X'
Tactic: ⟨Y, Z, f, g, h, hT, hP, hQ⟩
-- 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 Q R : ObjectProperty.{v_1, u_1} C
X X' : C
i : X ≅ X'
Y Z : C
f : Y ⟶ X
g : X ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) Y
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hP : P Y
hQ : Q Z
⊢ P.extensionProduct Q X'
have refine : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
  (Triangle.mk (f ≫ i.hom) (i.inv ≫ g) h)
Tactic: refine ⟨Y, Z, f ≫ i.hom, i.inv ≫ g, h, ?_, hP, hQ⟩
-- 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 Q : ObjectProperty.{v_1, u_1} C
⊢ P.isoClosure.extensionProduct Q = P.extensionProduct Q
have refine : P.isoClosure.extensionProduct Q ≤ P.extensionProduct Q
Tactic: refine le_antisymm ?_ (monotone_extensionProduct_left Q P.le_isoClosure)