awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : n < j
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)
have this : t.IsLE X (j - 1)
Tactic: have := t.isLE_of_le X n (j - 1) (by lia)
-- 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
j : EInt
hj : WithBotTop.coe n < j
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj j).obj X)
have bot : ∀ (hj : WithBotTop.coe n < ⊥), IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊥).obj X)
Tactic: induction j using WithBotTop.rec with
  | bot => simp at hj
  | coe j =>
    simp only [WithBotTop.coe_lt_coe] at hj
    have := t.isLE_of_le X n (j - 1) (by lia)
    exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _
  | top => simp
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.IsLE X n
j : EInt
hj : WithBotTop.coe n < j
bot : ∀ (hj : WithBotTop.coe n < ⊥), IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊥).obj X)
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj j).obj X)
have coe : ∀ (j : ℤ) (hj : WithBotTop.coe n < WithBotTop.coe j), IsZero.{v_1, u_1} ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)
Tactic: induction j using WithBotTop.rec with
  | bot => simp at hj
  | coe j =>
    simp only [WithBotTop.coe_lt_coe] at hj
    have := t.isLE_of_le X n (j - 1) (by lia)
    exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _
  | top => simp
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.IsLE X n
j : EInt
hj : WithBotTop.coe n < j
bot : ∀ (hj : WithBotTop.coe n < ⊥), IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊥).obj X)
coe :
  ∀ (j : ℤ) (hj : WithBotTop.coe n < WithBotTop.coe j), IsZero.{v_1, u_1} ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj j).obj X)
have top : ∀ (hj : WithBotTop.coe n < ⊤), IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊤).obj X)
Tactic: induction j using WithBotTop.rec with
  | bot => simp at hj
  | coe j =>
    simp only [WithBotTop.coe_lt_coe] at hj
    have := t.isLE_of_le X n (j - 1) (by lia)
    exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _
  | top => simp
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
inst_6 : IsTriangulated.{v_1, u_1} C
a : EInt
X : C
h : a ≤ ⊥
⊢ IsIso ((t.eTruncGE.obj ⊥).map ((t.eTruncGEπ a).app X))
have bot : ∀ (h : LE.le (α := EInt) ⊥ ⊥),
  IsIso (Y := (t.eTruncGE.obj ⊥).obj ((t.eTruncGE.obj ⊥).obj X))
    ((t.eTruncGE.obj ⊥).map (NatTrans.app (t.eTruncGEπ ⊥) X))
Tactic: obtain rfl : a = ⊥ := by simpa using h
Cleared hypotheses: a, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a : EInt
X : C
b : ℤ
h : a ≤ WithBotTop.coe b
⊢ IsIso ((t.eTruncGE.obj (WithBotTop.coe b)).map ((t.eTruncGEπ a).app X))
have coe : ∀ (h : ⊥ ≤ WithBotTop.coe b),
  IsIso (Y := (t.eTruncGE.obj (WithBotTop.coe b)).obj ((t.eTruncGE.obj ⊥).obj X))
    ((t.eTruncGE.obj (WithBotTop.coe b)).map (NatTrans.app (t.eTruncGEπ ⊥) X))
Tactic: induction a using WithBotTop.rec with
    | bot => infer_instance
    | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X
    | top => simp at h
Cleared hypotheses: a, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a : EInt
X : C
b : ℤ
h : a ≤ WithBotTop.coe b
coe :
  ∀ (h : ⊥ ≤ WithBotTop.coe b),
    IsIso (Y := (t.eTruncGE.obj (WithBotTop.coe b)).obj ((t.eTruncGE.obj ⊥).obj X))
      ((t.eTruncGE.obj (WithBotTop.coe b)).map (NatTrans.app (t.eTruncGEπ ⊥) X))
⊢ IsIso ((t.eTruncGE.obj (WithBotTop.coe b)).map ((t.eTruncGEπ a).app X))
have coe₁ : ∀ (a : ℤ) (h : WithBotTop.coe a ≤ WithBotTop.coe b),
  IsIso (Y := (t.eTruncGE.obj (WithBotTop.coe b)).obj ((t.eTruncGE.obj (WithBotTop.coe a)).obj X))
    ((t.eTruncGE.obj (WithBotTop.coe b)).map (NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) X))
Tactic: induction a using WithBotTop.rec with
    | bot => infer_instance
    | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X
    | top => simp at h
Cleared hypotheses: a, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a : EInt
X : C
b : ℤ
h : a ≤ WithBotTop.coe b
coe :
  ∀ (h : ⊥ ≤ WithBotTop.coe b),
    IsIso (Y := (t.eTruncGE.obj (WithBotTop.coe b)).obj ((t.eTruncGE.obj ⊥).obj X))
      ((t.eTruncGE.obj (WithBotTop.coe b)).map (NatTrans.app (t.eTruncGEπ ⊥) X))
coe₁ :
  ∀ (a : ℤ) (h : WithBotTop.coe a ≤ WithBotTop.coe b),
    IsIso (Y := (t.eTruncGE.obj (WithBotTop.coe b)).obj ((t.eTruncGE.obj (WithBotTop.coe a)).obj X))
      ((t.eTruncGE.obj (WithBotTop.coe b)).map (NatTrans.app (t.eTruncGEπ (WithBotTop.coe a)) X))
⊢ IsIso ((t.eTruncGE.obj (WithBotTop.coe b)).map ((t.eTruncGEπ a).app X))
have coe₂ : ∀ (h : ⊤ ≤ WithBotTop.coe b),
  IsIso (Y := (t.eTruncGE.obj (WithBotTop.coe b)).obj ((t.eTruncGE.obj ⊤).obj X))
    ((t.eTruncGE.obj (WithBotTop.coe b)).map (NatTrans.app (t.eTruncGEπ ⊤) X))
Tactic: induction a using WithBotTop.rec with
    | bot => infer_instance
    | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X
    | top => simp at h
Cleared hypotheses: a, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
h : a ≤ b
X : C
⊢ IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
have bot : ∀ (h : a ≤ ⊥), IsIso ((t.eTruncGE.obj ⊥).map ((t.eTruncGEπ a).app X))
Tactic: induction b using WithBotTop.rec with
  | bot =>
    obtain rfl : a = ⊥ := by simpa using h
    infer_instance
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => infer_instance
    | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X
    | top => simp at h
  | top => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩
Cleared hypotheses: b, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
h : a ≤ b
X : C
bot : ∀ (h : a ≤ ⊥), IsIso ((t.eTruncGE.obj ⊥).map ((t.eTruncGEπ a).app X))
⊢ IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
have coe : ∀ (b : ℤ) (h : a ≤ WithBotTop.coe b), IsIso ((t.eTruncGE.obj (WithBotTop.coe b)).map ((t.eTruncGEπ a).app X))
Tactic: induction b using WithBotTop.rec with
  | bot =>
    obtain rfl : a = ⊥ := by simpa using h
    infer_instance
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => infer_instance
    | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X
    | top => simp at h
  | top => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩
Cleared hypotheses: b, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
h : a ≤ b
X : C
bot : ∀ (h : a ≤ ⊥), IsIso ((t.eTruncGE.obj ⊥).map ((t.eTruncGEπ a).app X))
coe : ∀ (b : ℤ) (h : a ≤ WithBotTop.coe b), IsIso ((t.eTruncGE.obj (WithBotTop.coe b)).map ((t.eTruncGEπ a).app X))
⊢ IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
have top : ∀ (h : a ≤ ⊤), IsIso ((t.eTruncGE.obj ⊤).map ((t.eTruncGEπ a).app X))
Tactic: induction b using WithBotTop.rec with
  | bot =>
    obtain rfl : a = ⊥ := by simpa using h
    infer_instance
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => infer_instance
    | coe a => exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X
    | top => simp at h
  | top => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩
Cleared hypotheses: b, 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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
a : ℤ
h : WithBotTop.coe a ≤ ⊤
⊢ IsIso (X := (t.eTruncLT.obj (WithBotTop.coe a)).obj ((t.eTruncLT.obj ⊤).obj X))
    ((t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι ⊤) X))
have coe : IsIso ((t.truncLT a).map (𝟙 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
inst_6 : IsTriangulated.{v_1, u_1} C
b : EInt
X : C
a : ℤ
h : WithBotTop.coe a ≤ b
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι b).app X))
have coe : ∀ (h : WithBotTop.coe a ≤ ⊥),
  IsIso (X := (t.eTruncLT.obj (WithBotTop.coe a)).obj ((t.eTruncLT.obj ⊥).obj X))
    ((t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι ⊥) X))
Tactic: induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance
Cleared hypotheses: b, 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
inst_6 : IsTriangulated.{v_1, u_1} C
b : EInt
X : C
a : ℤ
h : WithBotTop.coe a ≤ b
coe :
  ∀ (h : WithBotTop.coe a ≤ ⊥),
    IsIso (X := (t.eTruncLT.obj (WithBotTop.coe a)).obj ((t.eTruncLT.obj ⊥).obj X))
      ((t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι ⊥) X))
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι b).app X))
have coe₁ : ∀ (b : ℤ) (h : WithBotTop.coe a ≤ WithBotTop.coe b),
  IsIso (X := (t.eTruncLT.obj (WithBotTop.coe a)).obj ((t.eTruncLT.obj (WithBotTop.coe b)).obj X))
    ((t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι (WithBotTop.coe b)) X))
Tactic: induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance
Cleared hypotheses: b, 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
inst_6 : IsTriangulated.{v_1, u_1} C
b : EInt
X : C
a : ℤ
h : WithBotTop.coe a ≤ b
coe :
  ∀ (h : WithBotTop.coe a ≤ ⊥),
    IsIso (X := (t.eTruncLT.obj (WithBotTop.coe a)).obj ((t.eTruncLT.obj ⊥).obj X))
      ((t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι ⊥) X))
coe₁ :
  ∀ (b : ℤ) (h : WithBotTop.coe a ≤ WithBotTop.coe b),
    IsIso (X := (t.eTruncLT.obj (WithBotTop.coe a)).obj ((t.eTruncLT.obj (WithBotTop.coe b)).obj X))
      ((t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι (WithBotTop.coe b)) X))
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι b).app X))
have coe₂ : ∀ (h : WithBotTop.coe a ≤ ⊤),
  IsIso (X := (t.eTruncLT.obj (WithBotTop.coe a)).obj ((t.eTruncLT.obj ⊤).obj X))
    ((t.eTruncLT.obj (WithBotTop.coe a)).map (NatTrans.app (t.eTruncLTι ⊤) X))
Tactic: induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance
Cleared hypotheses: b, 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
inst_6 : IsTriangulated.{v_1, u_1} C
b : EInt
X : C
h : ⊤ ≤ b
⊢ IsIso ((t.eTruncLT.obj ⊤).map ((t.eTruncLTι b).app X))
have top : ∀ (h : LE.le (α := EInt) ⊤ ⊤),
  IsIso (X := (t.eTruncLT.obj ⊤).obj ((t.eTruncLT.obj ⊤).obj X))
    ((t.eTruncLT.obj ⊤).map (NatTrans.app (t.eTruncLTι ⊤) X))
Tactic: obtain rfl : b = ⊤ := by simpa using h
Cleared hypotheses: b, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
h : a ≤ b
X : C
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X))
have bot : ∀ (h : ⊥ ≤ b), IsIso ((t.eTruncLT.obj ⊥).map ((t.eTruncLTι b).app X))
Tactic: induction a using WithBotTop.rec with
  | bot => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩
  | coe a =>
    induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance
  | top =>
    obtain rfl : b = ⊤ := by simpa using h
    infer_instance
Cleared hypotheses: a, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
h : a ≤ b
X : C
bot : ∀ (h : ⊥ ≤ b), IsIso ((t.eTruncLT.obj ⊥).map ((t.eTruncLTι b).app X))
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X))
have coe : ∀ (a : ℤ) (h : WithBotTop.coe a ≤ b), IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι b).app X))
Tactic: induction a using WithBotTop.rec with
  | bot => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩
  | coe a =>
    induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance
  | top =>
    obtain rfl : b = ⊤ := by simpa using h
    infer_instance
Cleared hypotheses: a, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a b : EInt
h : a ≤ b
X : C
bot : ∀ (h : ⊥ ≤ b), IsIso ((t.eTruncLT.obj ⊥).map ((t.eTruncLTι b).app X))
coe : ∀ (a : ℤ) (h : WithBotTop.coe a ≤ b), IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι b).app X))
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι b).app X))
have top : ∀ (h : ⊤ ≤ b), IsIso ((t.eTruncLT.obj ⊤).map ((t.eTruncLTι b).app X))
Tactic: induction a using WithBotTop.rec with
  | bot => exact ⟨0, IsZero.eq_of_src (by simp) _ _, IsZero.eq_of_src (by simp) _ _⟩
  | coe a =>
    induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance
  | top =>
    obtain rfl : b = ⊤ := by simpa using h
    infer_instance
Cleared hypotheses: a, 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
inst_6 : IsTriangulated.{v_1, u_1} C
a : EInt
X : C
⊢ IsIso (X := (t.eTruncLT.obj a).obj ((t.eTruncLT.obj a).obj X)) ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X))
have rw : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))
Tactic: rw [← eTruncLT_obj_map_eTruncLTι_app]
-- 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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsGE X n
a : ℤ
⊢ t.IsGE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n
have coe : t.IsGE ((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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsGE X n
i : EInt
⊢ t.IsGE ((t.eTruncLT.obj i).obj X) n
have bot : t.IsGE ((t.eTruncLT.obj ⊥).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact isGE_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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsGE X n
i : EInt
bot : t.IsGE ((t.eTruncLT.obj ⊥).obj X) n
⊢ t.IsGE ((t.eTruncLT.obj i).obj X) n
have coe : ∀ (a : ℤ), t.IsGE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact isGE_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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsGE X n
i : EInt
bot : t.IsGE ((t.eTruncLT.obj ⊥).obj X) n
coe : ∀ (a : ℤ), t.IsGE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n
⊢ t.IsGE ((t.eTruncLT.obj i).obj X) n
have top : t.IsGE ((t.eTruncLT.obj ⊤).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => exact isGE_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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsLE X n
a : ℤ
⊢ t.IsLE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n
have coe : t.IsLE ((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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsLE X n
i : EInt
⊢ t.IsLE ((t.eTruncGE.obj i).obj X) n
have bot : t.IsLE ((t.eTruncGE.obj ⊥).obj X) n
Tactic: induction i using WithBotTop.rec with
  | bot => dsimp; infer_instance
  | coe _ => dsimp; infer_instance
  | top => exact isLE_of_isZero _ (by simp) _
Cleared hypotheses: i