awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
⊢ t.IsGE ((t.triangleLTGE b).obj X).obj₃ a
have dsimp : t.IsGE ((t.truncGE b).obj X) a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
⊢ IsZero.{v, u} ((t.truncLT a).obj ((t.truncLT b).obj X))
have this : IsIso ((t.truncLT a).map ((t.triangleLTGE b).obj X).mor₁)
Tactic: have := t.isIso₁_truncLT_map_of_isGE _ ((t.triangleLTGE_distinguished b X)) a
    (by dsimp; infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ IsZero.{v, u} ((t.truncLT a).obj ((t.truncLT b).obj X))
have refine : IsZero.{v, u} ((t.truncLT a).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))
Tactic: refine IsZero.of_iso ?_ (asIso ((t.truncLT a).map ((t.truncLTι b).app X)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsGE X a
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ IsZero.{v, u} ((t.truncLT a).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))
have rwa : t.IsGE (Functor.obj.{v, v, u, u} (𝟭 C) X) a
Tactic: rwa [← isGE_iff_isZero_truncLT_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
⊢ t.IsLE ((t.truncGE a).obj X) b
have rw : IsZero.{v, u} ((t.truncGE (b + 1)).obj ((t.truncGE a).obj X))
Tactic: rw [t.isLE_iff_isZero_truncGE_obj b (b + 1) rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
⊢ t.IsLE ((t.triangleLTGE a).obj X).obj₁ b
have dsimp : t.IsLE ((t.truncLT a).obj X) b
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
⊢ IsZero.{v, u} ((t.truncGE (b + 1)).obj ((t.truncGE a).obj X))
have this : IsIso ((t.truncGE (b + 1)).map ((t.triangleLTGE a).obj X).mor₂)
Tactic: have := t.isIso₂_truncGE_map_of_isLE _ (t.triangleLTGE_distinguished a X) b _ rfl
    (by dsimp; infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
this : IsIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))
⊢ IsZero.{v, u} ((t.truncGE (b + 1)).obj ((t.truncGE a).obj X))
have refine : IsZero.{v, u} ((t.truncGE (b + 1)).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))
Tactic: refine IsZero.of_iso ?_ (asIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
inst_7 : t.IsLE X b
this : IsIso ((t.truncGE (b + 1)).map ((t.truncGEπ a).app X))
⊢ IsZero.{v, u} ((t.truncGE (b + 1)).obj (Functor.obj.{v, v, u, u} (𝟭 C) X))
have rwa : t.IsLE (Functor.obj.{v, v, u, u} (𝟭 C) X) b
Tactic: rwa [← isLE_iff_isZero_truncGE_obj _ _ _ rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
⊢ t.IsLE ((t.truncGELT a b).obj X) (b - 1)
have dsimp : t.IsLE ((t.truncGE a).obj ((t.truncLT b).obj X)) (b - 1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
X : C
a b : ℤ
⊢ t.IsGE ((t.truncLTGE a b).obj X) a
have dsimp : t.IsGE ((t.truncLT b).obj ((t.truncGE a).obj X)) a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ IsIso (X := (t.truncLT b).obj ((t.truncGE a).obj ((t.truncLT b).obj X)))
    ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))
have rw : t.IsLE ((t.truncGE a).obj ((t.truncLT b).obj X)) (b - 1)
Tactic: rw [← t.isLE_iff_isIso_truncLTι_app (b - 1) b (by lia)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
x x_1 : C
x_2 : x ⟶ x_1
⊢ ((t.truncGELT a b).map x_2 ≫
        t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x_1 ≫ (t.truncGEπ a).app x_1) a) (b - 1) b ⋯) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_1) =
    (t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x ≫ (t.truncGEπ a).app x) a) (b - 1) b ⋯ ≫
        (t.truncLTGE a b).map x_2) ≫
      (t.truncLTι b).app ((t.truncGE a).obj x_1)
have dsimp : ((t.truncGE a).map ((t.truncLT b).map x_2) ≫
      t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x_1 ≫ (t.truncGEπ a).app x_1) a) (b - 1) b sorry) ≫
    (t.truncLTι b).app ((t.truncGE a).obj x_1) =
  (t.liftTruncLT (t.descTruncGE ((t.truncLTι b).app x ≫ (t.truncGEπ a).app x) a) (b - 1) b sorry ≫
      (t.truncLT b).map ((t.truncGE a).map x_2)) ≫
    (t.truncLTι b).app ((t.truncGE a).obj x_1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ (t.truncGELTToLTGE a b).app X =
    (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))
have rw : (t.truncGELTToLTGE a b).app X =
  inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X))) ≫
    (t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X))
Tactic: rw [← cancel_epi (inv ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)))),
    IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleLTLTGELT a b h).obj X)
have this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
Tactic: have := t.isIso_truncLT_map_truncLTι_app a b h X
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.triangleLTLTGELT a b h).obj X)
have refine : (t.triangleLTLTGELT a b h).obj X ≅ (t.triangleLTGE a).obj ((t.truncLT b).obj X)
Tactic: refine isomorphic_distinguished _ (t.triangleLTGE_distinguished a ((t.truncLT b).obj X)) _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ (t.triangleLTLTGELT a b h).obj X ≅ (t.triangleLTGE a).obj ((t.truncLT b).obj X)
have refine : ((t.triangleLTLTGELT a b h).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₂) =
  (asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm.hom ≫ ((t.triangleLTGE a).obj ((t.truncLT b).obj X)).mor₁
Tactic: refine Triangle.isoMk _ _ ((asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm)
    (Iso.refl _) (Iso.refl _) ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ ((t.triangleLTLTGELT a b h).obj X).mor₁ ≫ Iso.hom (Iso.refl ((t.triangleLTLTGELT a b h).obj X).obj₂) =
    (asIso ((t.truncLT a).map ((t.truncLTι b).app X))).symm.hom ≫ ((t.triangleLTGE a).obj ((t.truncLT b).obj X)).mor₁
have dsimp : (t.natTransTruncLTOfLE a b h).app X ≫ 𝟙 ((t.truncLT b).obj X) =
  inv ((t.truncLT a).map ((t.truncLTι b).app X)) ≫ (t.truncLTι a).app ((t.truncLT b).obj X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
h : a ≤ b
X : C
this : IsIso ((t.truncLT a).map ((t.truncLTι b).app X))
⊢ (t.natTransTruncLTOfLE a b h).app X ≫ 𝟙 ((t.truncLT b).obj X) =
    inv ((t.truncLT a).map ((t.truncLTι b).app X)) ≫ (t.truncLTι a).app ((t.truncLT b).obj X)
have simp : (t.truncLT a).map ((t.truncLTι b).app X) ≫ (t.natTransTruncLTOfLE a b h).app X =
  (t.truncLTι a).app ((t.truncLT b).obj X)
Tactic: simp only [Category.comp_id, IsIso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
⊢ IsIso (t.truncGELTToLTGE a b)
have rw : ∀ (X : C), IsIso ((t.truncGELTToLTGE a b).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have pos : ∀ (h : a ≤ b), IsIso ((t.truncGELTToLTGE a b).app X)
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
pos : ∀ (h : a ≤ b), IsIso ((t.truncGELTToLTGE a b).app X)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have neg : ∀ (h : ¬a ≤ b), IsIso ((t.truncGELTToLTGE a b).app X)
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have eq : u₁₂ ≫ u₂₃ = u₁₃
Tactic: have eq : u₁₂ ≫ u₂₃ = u₁₃ := by simp [u₁₂, u₂₃, u₁₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have pos : ∀ (H : Octahedron eq sorry sorry sorry), IsIso ((t.truncGELTToLTGE a b).app X)
Tactic: have H := someOctahedron eq (t.triangleLTLTGELT_distinguished a b h X)
      (t.triangleLTGE_distinguished b X) (t.triangleLTGE_distinguished a X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
⊢ t.IsGE
    (Triangle.mk H.m₁ H.m₃
        ((t.truncGEδLT b).app X ≫
          Functor.map (shiftFunctor C (A := ℤ) 1) (((t.truncLT b).whiskerLeft (t.truncGEπ a)).app X))).obj₃
    b
have dsimp : t.IsGE ((t.truncGE b).obj X) b
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have this : IsIso ((t.truncLT b).map H.m₁)
Tactic: have : IsIso ((t.truncLT b).map H.m₁) :=
      t.isIso₁_truncLT_map_of_isGE _ H.mem b (by dsimp; infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have eq' : t.liftTruncLT m₁ (b - 1) b sorry = (t.truncGELTToLTGE a b).app X
Tactic: have eq' : t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncGELTToLTGE a b).app X :=
      t.to_truncLT_obj_ext
        (by dsimp; exact t.from_truncGE_obj_ext (by simpa using H.comm₁))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have pos : IsIso (t.liftTruncLT m₁ (b - 1) b sorry)
Tactic: rw [← eq']
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
⊢ IsIso (t.liftTruncLT m₁ (b - 1) b ⋯)
have fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ t.liftTruncLT m₁ (b - 1) b sorry = (t.truncLT b).map m₁
Tactic: have fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫
        t.liftTruncLT m₁ (b - 1) b (by lia) = (t.truncLT b).map m₁ :=
      t.to_truncLT_obj_ext (by simp [truncGELT])
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : ¬a ≤ b
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have h₁ : b < a
Tactic: simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : b < a
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have neg : (t.truncGELTToLTGE a b).app X ≫ 0 = 𝟙 ((t.truncGELT a b).obj X)
Tactic: refine ⟨0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
h : b < a
neg : (t.truncGELTToLTGE a b).app X ≫ 0 = 𝟙 ((t.truncGELT a b).obj X)
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
have neg₁ : 0 ≫ (t.truncGELTToLTGE a b).app X = 𝟙 ((t.truncLTGE a b).obj X)
Tactic: refine ⟨0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
t : TStructure.{v, u} C
inst_6 : IsTriangulated.{v, u} C
a b : ℤ
X : C
⊢ IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))
have rw : IsIso ((t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ (t.truncGELTToLTGE a b).app X)
Tactic: rw [← t.truncLT_map_truncGE_map_truncLTι_app_fac a b X]