awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
i j : EInt
f : i ⟶ j
X : C
bot :
  ∀ (f : i ⟶ ⊥),
    Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊥).obj X) ⟶ (t.eTruncLT.obj ⊥).obj X)
      ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
      (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj ⊥).obj X))
coe :
  ∀ (a : ℤ) (f : i ⟶ WithBotTop.coe a),
    Eq (α :=
      (t.eTruncLT.obj i).obj ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) ⟶ (t.eTruncLT.obj (WithBotTop.coe a)).obj X)
      ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE ⋯)) X) ≫ (t.eTruncLT.map f).app X)
      (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj (WithBotTop.coe a)).obj X))
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    NatTrans.app (t.eTruncLT.map (f ≫ homOfLE ⋯)) ((t.eTruncLT.obj j).obj X)
have top : ∀ (f : i ⟶ ⊤),
  Eq (α := (t.eTruncLT.obj i).obj ((t.eTruncLT.obj ⊤).obj X) ⟶ (t.eTruncLT.obj ⊤).obj X)
    ((t.eTruncLT.obj i).map (NatTrans.app (t.eTruncLT.map (homOfLE sorry)) X) ≫ (t.eTruncLT.map f).app X)
    (NatTrans.app (t.eTruncLT.map (f ≫ homOfLE sorry)) ((t.eTruncLT.obj ⊤).obj X))
Tactic: induction j using WithBotTop.rec with simp [truncLT_map_truncLTι_app]
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊥).obj X)
have bot : IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂
Tactic: rw [Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂
have bot : IsIso.{v_1, u_1} (𝟙 X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊤).obj X)
have top : IsIso ((t.eTriangleLTGE.obj ⊤).obj X).mor₁
Tactic: rw [Triangle.distinguished_iff_of_isZero₃ _ (Functor.zero_obj X)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊤).obj X).mor₁
have top : IsIso.{v_1, u_1} (𝟙 X)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
i : EInt
X : C
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj i).obj X)
have bot : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
  ((t.eTriangleLTGE.obj ⊥).obj X)
Tactic: induction i using WithBotTop.rec with
  | bot =>
    rw [Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)]
    dsimp
    infer_instance
  | coe n => exact t.triangleLTGE_distinguished n X
  | top =>
    rw [Triangle.distinguished_iff_of_isZero₃ _ (Functor.zero_obj X)]
    dsimp
    infer_instance
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
i : EInt
X : C
bot :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊥).obj X)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj i).obj X)
have coe : ∀ (n : ℤ),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj (WithBotTop.coe n)).obj X)
Tactic: induction i using WithBotTop.rec with
  | bot =>
    rw [Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)]
    dsimp
    infer_instance
  | coe n => exact t.triangleLTGE_distinguished n X
  | top =>
    rw [Triangle.distinguished_iff_of_isZero₃ _ (Functor.zero_obj X)]
    dsimp
    infer_instance
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
i : EInt
X : C
bot :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj ⊥).obj X)
coe :
  ∀ (n : ℤ),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
      ((t.eTriangleLTGE.obj (WithBotTop.coe n)).obj X)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
    ((t.eTriangleLTGE.obj i).obj X)
have top : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_1 inst_4 _)
  ((t.eTriangleLTGE.obj ⊤).obj X)
Tactic: induction i using WithBotTop.rec with
  | bot =>
    rw [Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)]
    dsimp
    infer_instance
  | coe n => exact t.triangleLTGE_distinguished n X
  | top =>
    rw [Triangle.distinguished_iff_of_isZero₃ _ (Functor.zero_obj X)]
    dsimp
    infer_instance
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsLE X n
a : ℤ
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n
have coe : t.IsLE ((t.truncLT a).obj X) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsLE X n
i : EInt
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n
have bot : t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact isLE_of_isZero _ (by simp) _
  | coe _ => dsimp; infer_instance
  | top => dsimp; infer_instance
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsLE X n
i : EInt
bot : t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n
have coe : ∀ (a : ℤ), t.IsLE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact isLE_of_isZero _ (by simp) _
  | coe _ => dsimp; infer_instance
  | top => dsimp; infer_instance
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsLE X n
i : EInt
bot : t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
coe : ∀ (a : ℤ), t.IsLE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n
have top : t.IsLE ((t.eTruncLT.obj ⊤).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact isLE_of_isZero _ (by simp) _
  | coe _ => dsimp; infer_instance
  | top => dsimp; infer_instance
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsGE X n
a : ℤ
⊢ t.IsGE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n
have coe : t.IsGE ((t.truncGE a).obj X) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsGE X n
i : EInt
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n
have bot : t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => dsimp; infer_instance
  | coe _ => dsimp; infer_instance
  | top => exact isGE_of_isZero _ (by simp) _
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsGE X n
i : EInt
bot : t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n
have coe : ∀ (a : ℤ), t.IsGE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => dsimp; infer_instance
  | coe _ => dsimp; infer_instance
  | top => exact isGE_of_isZero _ (by simp) _
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsGE X n
i : EInt
bot : t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
coe : ∀ (a : ℤ), t.IsGE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n
have top : t.IsGE ((t.eTruncGE.obj ⊤).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => dsimp; infer_instance
  | coe _ => dsimp; infer_instance
  | top => exact isGE_of_isZero _ (by simp) _
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
X : C
i : ℤ
h : WithBotTop.coe n ≤ WithBotTop.coe i
⊢ t.IsGE ((t.eTruncGE.obj (WithBotTop.coe i)).obj X) n
have coe : t.IsGE ((t.truncGE i).obj X) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
i : EInt
h : WithBotTop.coe n ≤ i
X : C
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n
have bot : ∀ (h : WithBotTop.coe n ≤ ⊥), t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => simp at h
  | coe i =>
    dsimp
    exact t.isGE_of_ge _ _ _ (by simpa using h)
  | top => exact t.isGE_of_isZero (Functor.zero_obj _) _
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
i : EInt
h : WithBotTop.coe n ≤ i
X : C
bot : ∀ (h : WithBotTop.coe n ≤ ⊥), t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n
have coe : ∀ (i : ℤ) (h : WithBotTop.coe n ≤ WithBotTop.coe i), t.IsGE ((t.eTruncGE.obj (WithBotTop.coe i)).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => simp at h
  | coe i =>
    dsimp
    exact t.isGE_of_ge _ _ _ (by simpa using h)
  | top => exact t.isGE_of_isZero (Functor.zero_obj _) _
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
i : EInt
h : WithBotTop.coe n ≤ i
X : C
bot : ∀ (h : WithBotTop.coe n ≤ ⊥), t.IsGE ((t.eTruncGE.obj ⊥).obj X) n
coe : ∀ (i : ℤ) (h : WithBotTop.coe n ≤ WithBotTop.coe i), t.IsGE ((t.eTruncGE.obj (WithBotTop.coe i)).obj X) n
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n
have top : ∀ (h : WithBotTop.coe n ≤ ⊤), t.IsGE ((t.eTruncGE.obj ⊤).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => simp at h
  | coe i =>
    dsimp
    exact t.isGE_of_ge _ _ _ (by simpa using h)
  | top => exact t.isGE_of_isZero (Functor.zero_obj _) _
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (hypothesis)
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
n : ℤ
X : C
i : ℤ
h : WithBotTop.coe i ≤ WithBotTop.coe (n + 1)
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n
have h₁ : i ≤ n + 1
Tactic: simp only [WithBotTop.coe_le_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
X : C
i : ℤ
h : i ≤ n + 1
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n
have coe : t.IsLE ((t.truncLT i).obj X) n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
i : EInt
h : i ≤ WithBotTop.coe (n + 1)
X : C
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n
have bot : ∀ (h : ⊥ ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact t.isLE_of_isZero (by simp) _
  | coe i =>
    simp only [WithBotTop.coe_le_coe] at h
    dsimp
    exact t.isLE_of_le _ (i - 1) n (by lia)
  | top => simp at h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
i : EInt
h : i ≤ WithBotTop.coe (n + 1)
X : C
bot : ∀ (h : ⊥ ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n
have coe : ∀ (i : ℤ) (h : WithBotTop.coe i ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact t.isLE_of_isZero (by simp) _
  | coe i =>
    simp only [WithBotTop.coe_le_coe] at h
    dsimp
    exact t.isLE_of_le _ (i - 1) n (by lia)
  | top => simp at h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
n : ℤ
i : EInt
h : i ≤ WithBotTop.coe (n + 1)
X : C
bot : ∀ (h : ⊥ ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
coe : ∀ (i : ℤ) (h : WithBotTop.coe i ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n
have top : ∀ (h : ⊤ ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj ⊤).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact t.isLE_of_isZero (by simp) _
  | coe i =>
    simp only [WithBotTop.coe_le_coe] at h
    dsimp
    exact t.isLE_of_le _ (i - 1) n (by lia)
  | top => simp at h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (hypothesis)
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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : ℤ
hj : WithBotTop.coe j ≤ WithBotTop.coe n
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj (WithBotTop.coe j)).obj X)
have this : t.IsGE X j
Tactic: have := t.isGE_of_ge X j n (by simpa using hj)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : EInt
hj : j ≤ WithBotTop.coe n
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj j).obj X)
have bot : ∀ (hj : ⊥ ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊥).obj X)
Tactic: induction j using WithBotTop.rec with
  | bot => simp
  | coe j =>
    have := t.isGE_of_ge X j n (by simpa using hj)
    exact t.isZero_truncLT_obj_of_isGE _ _
  | top => simp at hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : EInt
hj : j ≤ WithBotTop.coe n
bot : ∀ (hj : ⊥ ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊥).obj X)
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj j).obj X)
have coe : ∀ (j : ℤ) (hj : WithBotTop.coe j ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj (WithBotTop.coe j)).obj X)
Tactic: induction j using WithBotTop.rec with
  | bot => simp
  | coe j =>
    have := t.isGE_of_ge X j n (by simpa using hj)
    exact t.isZero_truncLT_obj_of_isGE _ _
  | top => simp at hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : EInt
hj : j ≤ WithBotTop.coe n
bot : ∀ (hj : ⊥ ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊥).obj X)
coe :
  ∀ (j : ℤ) (hj : WithBotTop.coe j ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj (WithBotTop.coe j)).obj X)
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj j).obj X)
have top : ∀ (hj : ⊤ ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊤).obj X)
Tactic: induction j using WithBotTop.rec with
  | bot => simp
  | coe j =>
    have := t.isGE_of_ge X j n (by simpa using hj)
    exact t.isZero_truncLT_obj_of_isGE _ _
  | top => simp at hj
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (hypothesis)
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
X : C
n : ℤ
inst_6 : t.IsLE X n
j : ℤ
hj : WithBotTop.coe n < WithBotTop.coe j
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)
have hj₁ : n < j
Tactic: simp only [WithBotTop.coe_lt_coe] at hj
Cleared hypotheses: hj