awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
refine_1 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) =
    ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
          (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₁
refine_2 :
  ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫
      Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) =
    Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₂
⊢ (t.triangleω₁δ a b c hab hbc).obj X ≅ (t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)
have refine_3 : ((t.triangleω₁δ a b c hab hbc).obj X).mor₃ ≫
    Functor.map (shiftFunctor C (A := ℤ) 1)
      ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
          (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom =
  Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) ≫
    ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE sorry))).obj X)).mor₃
Tactic: refine Triangle.isoMk _ _ ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
    (t.eTruncLTGEIsoGELT a b).symm.app _) (Iso.refl _) ((t.eTruncGEIsoGEGE a b hab).app _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) =
    ((t.eTruncGE.obj a).mapIso ((t.eTruncLTLTIsoLT c b hbc).symm.app X) ≪≫
          (t.eTruncLTGEIsoGELT a b).symm.app ((t.eTruncLT.obj c).obj X)).hom ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₁
have refine_1 : ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ 𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) =
  ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
      (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X)) ≫
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₁ ≫ 𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) =
    ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
        (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X)) ≫
      (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
have refine_1 : (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
  (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
    (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
      (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
Tactic: simp only [triangleω₁δ_obj_mor₁, homOfLE_leOfHom, Category.comp_id, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ (t.eTruncGE.obj a).map ((t.eTruncLT.map (homOfLE hbc)).app X) =
    (t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).inv.app X) ≫
      (t.eTruncLTGEIsoGELT a b).inv.app ((t.eTruncLT.obj c).obj X) ≫
        (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
have refine_1 : Eq (α :=
  (t.eTruncGE.obj a ⋙ t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj X) ⟶
    (t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
  ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X) ≫
    (t.eTruncGE.obj a).map ((t.eTruncLTι b).app ((t.eTruncLT.obj c).obj X)))
  ((t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)))
Tactic: rw [← cancel_epi ((t.eTruncGE.obj a).map ((t.eTruncLTLTIsoLT c b hbc).hom.app X)),
      ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, Category.id_comp,
      ← cancel_epi ((t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj X)),
      Iso.hom_inv_id_app_assoc, eTruncLTLTIsoLT_hom, eTruncLTLTToLT_app,
      ← Functor.map_comp, eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
X : C
⊢ ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫
      Iso.hom ((t.eTruncGEIsoGEGE a b hab).app ((t.eTruncLT.obj ((mk₁ (homOfLE hbc)).obj 1)).obj X)) =
    Iso.hom (Iso.refl ((t.triangleω₁δ a b c hab hbc).obj X).obj₂) ≫
      ((t.eTriangleLTGE.obj b).obj ((t.ω₁.obj (mk₁ (homOfLE ⋯))).obj X)).mor₂
have refine_2 : ((t.triangleω₁δ a b c hab hbc).obj X).mor₂ ≫ (t.eTruncGEToGEGE a b).app ((t.eTruncLT.obj c).obj X) =
  𝟙 ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X)) ≫
    (t.eTruncGEπ b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj c).obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
D D' : ComposableArrows EInt 2
φ : D ⟶ D'
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
    (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ
have obtain : ∀ (a b c : EInt) (f : a ⟶ b) (g : b ⟶ c) (φ : mk₂ f g ⟶ D'),
  (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) sorry sorry).app X =
    (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) sorry sorry).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ
Tactic: obtain ⟨a, b, c, f, g, rfl⟩ := mk₂_surjective D
Cleared hypotheses: D, φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
D' : ComposableArrows EInt 2
a b c : EInt
f : a ⟶ b
g : b ⟶ c
φ : mk₂ f g ⟶ D'
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
    (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ
have obtain : ∀ (a' b' c' : EInt) (f' : a' ⟶ b') (g' : b' ⟶ c') (φ : mk₂ f g ⟶ mk₂ f' g'),
  (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        φ ≫
      (t.ω₁δ ((mk₂ f' g').obj 0) ((mk₂ f' g').obj 1) ((mk₂ f' g').obj 2) sorry sorry).app X =
    (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) sorry sorry).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ Functor.obj (evaluation C C) X) ⋙ shiftFunctor C (A := ℤ) 1).map
        φ
Tactic: obtain ⟨a', b', c', f', g', rfl⟩ := mk₂_surjective D'
Cleared hypotheses: D', φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
D : ComposableArrows EInt 2
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
            SpectralObject._proof_2 SpectralObject._proof_4)
          D))
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
            SpectralObject._proof_4 SpectralObject._proof_4)
          D))
      (NatTrans.app
        { app := fun (D : ComposableArrows EInt 2) ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X, naturality := ⋯ }
        D))
have obtain : ∀ (a b c : EInt) (f : a ⟶ b) (g : b ⟶ c),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    (Triangle.mk
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
            SpectralObject._proof_2 SpectralObject._proof_4)
          (mk₂ f g)))
      ((t.ω₁ ⋙ Functor.obj (evaluation C C) X).map
        (NatTrans.app
          (mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
            SpectralObject._proof_4 SpectralObject._proof_4)
          (mk₂ f g)))
      (NatTrans.app
        { app := fun (D : ComposableArrows EInt 2) ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) sorry sorry).app X, naturality := sorry }
        (mk₂ f g)))
Tactic: obtain ⟨a, b, c, f, g, rfl⟩ := mk₂_surjective D
Cleared hypotheses: D
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ t.truncLE a = t.truncLT b
have rw : t.truncLE a = t.truncLT (a + 1)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ t.truncGT a = t.truncGE b
have rw : t.truncGT a = t.truncGE (a + 1)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ (t.truncLEIsoTruncLT a b h).hom ≫ t.truncLTι b = t.truncLEι a
have subst : (t.truncLEIsoTruncLT a (a + 1) sorry).hom ≫ t.truncLTι (a + 1) = t.truncLEι a
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a : ℤ
⊢ 𝟙 (t.truncLE a) ≫ t.truncLTι (a + 1) = t.truncLTι (a + 1)
have rw : Eq (α := t.truncLE a ⟶ 𝟭 C) (t.truncLTι (a + 1)) (t.truncLTι (a + 1))
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ (t.truncLEIsoTruncLT a b h).inv ≫ t.truncLEι a = t.truncLTι b
have subst : (t.truncLEIsoTruncLT a (a + 1) sorry).inv ≫ t.truncLEι a = t.truncLTι (a + 1)
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a : ℤ
⊢ 𝟙 (t.truncLT (a + 1)) ≫ t.truncLTι (a + 1) = t.truncLTι (a + 1)
have rw : Eq (α := t.truncLT (a + 1) ⟶ 𝟭 C) (t.truncLTι (a + 1)) (t.truncLTι (a + 1))
Tactic: rw [Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ t.truncGTπ a ≫ (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b
have subst : t.truncGTπ a ≫ (t.truncGTIsoTruncGE a (a + 1) sorry).hom = t.truncGEπ (a + 1)
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a : ℤ
⊢ t.truncGEπ (a + 1) ≫ 𝟙 (t.truncGT a) = t.truncGEπ (a + 1)
have rw : Eq (α := 𝟭 C ⟶ t.truncGE (a + 1)) (t.truncGEπ (a + 1)) (t.truncGEπ (a + 1))
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ t.truncGEπ b ≫ (t.truncGTIsoTruncGE a b h).inv = t.truncGTπ a
have subst : t.truncGEπ (a + 1) ≫ (t.truncGTIsoTruncGE a (a + 1) sorry).inv = t.truncGTπ a
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a : ℤ
⊢ t.truncGEπ (a + 1) ≫ 𝟙 (t.truncGE (a + 1)) = t.truncGEπ (a + 1)
have rw : Eq (α := 𝟭 C ⟶ t.truncGE (a + 1)) (t.truncGEπ (a + 1)) (t.truncGEπ (a + 1))
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ t.triangleLEGE a b h ≅ t.triangleLTGE b
have refine_1 : (t.triangleLEGE a b h).whiskerLeft Triangle.π₁Toπ₂ ≫ Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)) =
  (t.truncLEIsoTruncLT a b h).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₁Toπ₂
Tactic: refine Triangle.functorIsoMk _ _ (t.truncLEIsoTruncLT a b h) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
refine_1 :
  (t.triangleLEGE a b h).whiskerLeft Triangle.π₁Toπ₂ ≫ Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)) =
    (t.truncLEIsoTruncLT a b h).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₁Toπ₂
⊢ t.triangleLEGE a b h ≅ t.triangleLTGE b
have refine_2 : (t.triangleLEGE a b h).whiskerLeft Triangle.π₂Toπ₃ ≫ Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) =
  Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₂Toπ₃
Tactic: refine Triangle.functorIsoMk _ _ (t.truncLEIsoTruncLT a b h) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
refine_1 :
  (t.triangleLEGE a b h).whiskerLeft Triangle.π₁Toπ₂ ≫ Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)) =
    (t.truncLEIsoTruncLT a b h).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₁Toπ₂
refine_2 :
  (t.triangleLEGE a b h).whiskerLeft Triangle.π₂Toπ₃ ≫ Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) =
    Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₂)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₂Toπ₃
⊢ t.triangleLEGE a b h ≅ t.triangleLTGE b
have refine_3 : (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
    Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1) =
  Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁
Tactic: refine Triangle.functorIsoMk _ _ (t.truncLEIsoTruncLT a b h) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1) =
    Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁
have refine_3 : ∀ (x : C),
  ((t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1)).app
      x =
    (Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
x : C
⊢ ((t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C (A := ℤ) 1)).app
      x =
    (Iso.hom (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)) ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁).app x
have refine_3 : ((t.truncGEδLT b).app x ≫ Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncLEIsoTruncLT a b h).inv.app x)) ≫
    Functor.map (shiftFunctor C (A := ℤ) 1) ((t.truncLEIsoTruncLT a b h).hom.app x) =
  𝟙 ((t.truncGE b).obj x) ≫ (t.truncGEδLT b).app x
Tactic: dsimp [truncGEδLE]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{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
t : TStructure.{v_1, u_1} C
a b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (Iso.hom (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁))) (shiftFunctor C (A := ℤ) 1) =
    (t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁
have w : ∀ (x : C),
  ((t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (Iso.hom (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁))) (shiftFunctor C (A := ℤ) 1)).app
      x =
    ((t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁).app x
Tactic: ext