awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 : ℤ
coe : IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))
⊢ 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:
simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 X))
⊢ 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:
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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, CategoryTheory.zero_map, CategoryTheory.Limits.isIsoZero_iff_source_target_isZero, CategoryTheory.Functor.map_zero, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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)))
coe₁ : IsZero.{v_1, u_1} ((t.truncLT b).obj (Functor.obj.{v_1, v_1, u_1, u_1} 0 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))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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)))

Tactic:
Functor.map_isZero _ (Functor.zero_obj _)

Premises used: CategoryTheory.Functor.zero_obj, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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)))

Tactic:
exact Functor.map_isZero _ (Functor.zero_obj _)

Premises used: CategoryTheory.Functor.zero_obj, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 X))

Tactic:
Functor.map_isZero _ (Functor.zero_obj _)

Premises used: CategoryTheory.Functor.zero_obj, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 X))

Tactic:
exact Functor.map_isZero _ (Functor.zero_obj _)

Premises used: CategoryTheory.Functor.zero_obj, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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)
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)

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 _)

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, CategoryTheory.zero_map, CategoryTheory.Limits.isIsoZero_iff_source_target_isZero, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.zero_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Functor.map_isZero, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 (X := (t.eTruncLT.obj ⊤ ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj ⊤).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a ⊤) X)

Tactic:
simpa using inferInstanceAs (IsIso (𝟙 _))
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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)
top :
  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)

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 (𝟙 _))

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, CategoryTheory.zero_map, CategoryTheory.Limits.isIsoZero_iff_source_target_isZero, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.zero_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Functor.map_isZero, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
rw : ∀ (X : C), IsIso ((t.eTruncLTGELTSelfToGELT a b).app X)
⊢ IsIso (t.eTruncLTGELTSelfToGELT a b)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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_1 X : C
⊢ IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊥ b) X)

Tactic:
simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X)))
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 ⊥ ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj ⊥).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) ⊥) X)

Tactic:
simpa [isIsoZero_iff_source_target_isZero] using
        (t.eTruncGE.obj a).map_isZero (Functor.zero_obj _)

Premises used: WithBotTop.coe, CategoryTheory.Limits.isIsoZero_iff_source_target_isZero, CategoryTheory.Functor.zero_obj, CategoryTheory.Functor.map_isZero, CategoryTheory.Triangulated.TStructure.eTruncGE, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 : ℤ
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)))
⊢ 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:
simp only [eTruncLT_obj_coe, eTruncGE_obj_coe, Functor.comp_obj, eTruncLTGELTSelfToGELT_app,
        eTruncLT_map_eq_truncLTι]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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.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:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 ⊤ ⋙ t.eTruncGE.obj (WithBotTop.coe a) ⋙ t.eTruncLT.obj ⊤).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT (WithBotTop.coe a) ⊤) X)

Tactic:
simpa using inferInstanceAs (IsIso (𝟙 _))
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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)
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)

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 (𝟙 _))

Premises used: WithBotTop.coe, CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.isIsoZero_iff_source_target_isZero, CategoryTheory.Functor.zero_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Functor.map_isZero, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app, CategoryTheory.Triangulated.TStructure.eTruncGE, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, CategoryTheory.Functor.obj, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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_1 X : C
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊤).obj ((t.eTruncLT.obj b).obj X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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_1 X : C
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊤).obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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_1 X : C
⊢ IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊤ ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊤ b) X)

Tactic:
exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _,
      IsZero.eq_of_src (by simp) _ _⟩
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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_1 X : C
bot :
  IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊥ ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊥ b) X)
coe :
  ∀ (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)
top :
  IsIso (X := (t.eTruncLT.obj b ⋙ t.eTruncGE.obj ⊤ ⋙ t.eTruncLT.obj b).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToGELT ⊤ b) X)
⊢ IsIso ((t.eTruncLTGELTSelfToGELT a b).app X)

Tactic:
induction a using WithBotTop.rec with
  | bot => simpa using inferInstanceAs (IsIso ((t.eTruncLTι b).app ((t.eTruncLT.obj b).obj X)))
  | coe a =>
    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 (𝟙 _))
  | top =>
    exact ⟨0, ((t.eTruncLT.obj b).map_isZero (by simp)).eq_of_src _ _,
      IsZero.eq_of_src (by simp) _ _⟩

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.isIsoZero_iff_source_target_isZero, CategoryTheory.Functor.zero_obj, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, CategoryTheory.Functor.map_isZero, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app, CategoryTheory.Triangulated.TStructure.eTruncGE, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, CategoryTheory.Functor.obj, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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 Y : C
f : X ⟶ Y
⊢ (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map f) ≫ (t.eTruncLTGEIsoGELT a b).hom.app Y =
    (t.eTruncLTGEIsoGELT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLT.obj b).map f)

Tactic:
(t.eTruncLTGEIsoGELT a b).hom.naturality f

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
⊢ (t.eTruncLT.obj b).map ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) ≫ (t.eTruncLTGEIsoGELT a b).hom.app X =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj X))

Tactic:
simp [eTruncLTGEIsoGELT]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT
-- Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
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
⊢ (t.eTruncLTGEIsoGELT a b).hom.app X ≫ (t.eTruncGE.obj a).map ((t.eTruncLTι b).app X) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X)

Tactic:
simp [eTruncLTGEIsoGELT]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT