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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsLE X n
i : EInt
bot : t.IsLE ((t.eTruncGE.obj ⊥).obj X) n
⊢ t.IsLE ((t.eTruncGE.obj i).obj X) n
have coe : ∀ (a : ℤ), t.IsLE ((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 isLE_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
inst_6 : IsTriangulated.{v_1, u_1} C
X : C
n : ℤ
inst_7 : t.IsLE X n
i : EInt
bot : t.IsLE ((t.eTruncGE.obj ⊥).obj X) n
coe : ∀ (a : ℤ), t.IsLE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n
⊢ t.IsLE ((t.eTruncGE.obj i).obj X) n
have top : 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
-- 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
hab : a ≤ b
⊢ IsIso (t.eTruncGEToGEGE a b)
have rw : ∀ (X : C), IsIso ((t.eTruncGEToGEGE a b).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_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
a b : EInt
hab : a ≤ b
X : C
⊢ IsIso ((t.eTruncGEToGEGE a b).app X)
have simp : IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
Tactic: simp only [Functor.comp_obj, eTruncGEToGEGE_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
a b : EInt
hab : b ≤ a
⊢ IsIso (t.eTruncLTLTToLT a b)
have rw : ∀ (X : C), IsIso ((t.eTruncLTLTToLT a b).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_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
a b : EInt
hab : b ≤ a
X : C
⊢ IsIso ((t.eTruncLTLTToLT a b).app X)
have simp : IsIso ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X))
Tactic: simp only [Functor.comp_obj, eTruncLTLTToLT_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
a b : EInt
⊢ IsIso (t.eTruncLTGELTSelfToLTGE a b)
have rw : ∀ (X : C), IsIso ((t.eTruncLTGELTSelfToLTGE a b).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_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
a_1 b_1 : EInt
X : C
b a : ℤ
⊢ IsIso (X :=
    (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE (WithBotTop.coe a) (WithBotTop.coe b)) X)
have coe : IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))
Tactic: simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
-- 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_1 : EInt
X : C
b : ℤ
⊢ IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj ⊤ ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE ⊤ (WithBotTop.coe b)) X)
have coe : IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 ((t.truncLT b).obj X))) ∧
  IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 X))
Tactic: simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
-- 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_1 : EInt
X : C
b : ℤ
⊢ IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 ((t.truncLT b).obj X))) ∧
    IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 X))
have coe : IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 ((t.truncLT b).obj X)))
Tactic: constructor
-- 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_1 : EInt
X : C
b : ℤ
coe : IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 ((t.truncLT b).obj X)))
⊢ IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 ((t.truncLT b).obj X))) ∧
    IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 X))
have coe₁ : IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 X))
Tactic: constructor
-- 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_1 : EInt
X : C
b : ℤ
⊢ IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a (WithBotTop.coe b)) X)
have coe : IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToLTGE ⊥ (WithBotTop.coe b)) X)
Tactic: induction a using WithBotTop.rec with
    | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))
    | coe a =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)
-- 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_1 : EInt
X : C
b : ℤ
coe :
  IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE ⊥ (WithBotTop.coe b)) X)
⊢ IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a (WithBotTop.coe b)) X)
have coe₁ : ∀ (a : ℤ),
  IsIso (X :=
    (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE (WithBotTop.coe a) (WithBotTop.coe b)) X)
Tactic: induction a using WithBotTop.rec with
    | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))
    | coe a =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)
-- 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_1 : EInt
X : C
b : ℤ
coe :
  IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE ⊥ (WithBotTop.coe b)) X)
coe₁ :
  ∀ (a : ℤ),
    IsIso (X :=
      (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
      (NatTrans.app (t.eTruncLTGELTSelfToLTGE (WithBotTop.coe a) (WithBotTop.coe b)) X)
⊢ IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a (WithBotTop.coe b)) X)
have coe₂ : IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj ⊤ ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToLTGE ⊤ (WithBotTop.coe b)) X)
Tactic: induction a using WithBotTop.rec with
    | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))
    | coe a =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)
-- 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
X : C
⊢ IsIso ((t.eTruncLTGELTSelfToLTGE a b).app X)
have bot : IsIso (X := (t.eTruncLT.obj ⊥ ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj ⊥).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToLTGE a ⊥) X)
Tactic: induction b using WithBotTop.rec with
  | bot => simp [isIsoZero_iff_source_target_isZero]
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))
    | coe a =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)
  | top => simpa using inferInstanceAs (IsIso (𝟙 _))
-- 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
X : C
bot :
  IsIso (X := (t.eTruncLT.obj ⊥ ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj ⊥).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a ⊥) X)
⊢ IsIso ((t.eTruncLTGELTSelfToLTGE a b).app X)
have coe : ∀ (b : ℤ),
  IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a (WithBotTop.coe b)) X)
Tactic: induction b using WithBotTop.rec with
  | bot => simp [isIsoZero_iff_source_target_isZero]
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))
    | coe a =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)
  | top => simpa using inferInstanceAs (IsIso (𝟙 _))
-- 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
X : C
bot :
  IsIso (X := (t.eTruncLT.obj ⊥ ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj ⊥).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a ⊥) X)
coe :
  ∀ (b : ℤ),
    IsIso (X := (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
      (NatTrans.app (t.eTruncLTGELTSelfToLTGE a (WithBotTop.coe b)) X)
⊢ IsIso ((t.eTruncLTGELTSelfToLTGE a b).app X)
have top : IsIso (X := (t.eTruncLT.obj ⊤ ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj ⊤).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToLTGE a ⊤) X)
Tactic: induction b using WithBotTop.rec with
  | bot => simp [isIsoZero_iff_source_target_isZero]
  | coe b =>
    induction a using WithBotTop.rec with
    | bot => simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))
    | coe a =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)
  | top => simpa using inferInstanceAs (IsIso (𝟙 _))
-- 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_1 b : EInt
X : C
⊢ IsIso (t.eTruncLTGELTSelfToGELT a b)
have rw : ∀ (X : C), IsIso ((t.eTruncLTGELTSelfToGELT a b).app X)
Tactic: rw [NatTrans.isIso_iff_isIso_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
a_1 b_1 b_2 : EInt
X_1 X : C
a b : ℤ
⊢ IsIso (X :=
    (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) (WithBotTop.coe b)) X)
have coe : 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)))
Tactic: simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]
-- 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_1 b_1 b : EInt
X_1 X : C
a : ℤ
⊢ IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) b) X)
have coe : IsIso (X := (t.eTruncLT.obj ⊥ ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj ⊥).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) ⊥) X)
Tactic: induction b using WithBotTop.rec with
    | bot => simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)
    | coe b =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top => simpa using inferInstanceAs (IsIso (𝟙 _))
-- 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_1 b_1 b : EInt
X_1 X : C
a : ℤ
coe :
  IsIso (X := (t.eTruncLT.obj ⊥ ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj ⊥).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) ⊥) X)
⊢ IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) b) X)
have coe₁ : ∀ (b : ℤ),
  IsIso (X :=
    (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) (WithBotTop.coe b)) X)
Tactic: induction b using WithBotTop.rec with
    | bot => simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)
    | coe b =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top => simpa using inferInstanceAs (IsIso (𝟙 _))
-- 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_1 b_1 b : EInt
X_1 X : C
a : ℤ
coe :
  IsIso (X := (t.eTruncLT.obj ⊥ ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj ⊥).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) ⊥) X)
coe₁ :
  ∀ (b : ℤ),
    IsIso (X :=
      (t.eTruncLT.obj (WithBotTop.coe b) ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj (WithBotTop.coe b)).obj X)
      (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) (WithBotTop.coe b)) X)
⊢ IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) b) X)
have coe₂ : IsIso (X := (t.eTruncLT.obj ⊤ ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj ⊤).obj X)
  (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) ⊤) X)
Tactic: induction b using WithBotTop.rec with
    | bot => simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)
    | coe b =>
      simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]
      infer_instance
    | top => simpa using inferInstanceAs (IsIso (𝟙 _))