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
X : C
a : ℤ
h : WithBotTop.coe a ≤ ⊤
⊢ IsIso ((t.truncLT a).map (𝟙 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
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))
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))

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
-- 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
b : EInt
X : C
h : ⊤ ≤ b
⊢ b = ⊤

Tactic:
simpa using h
-- 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
b : EInt
X : C
h : ⊤ ≤ b
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))
⊢ IsIso ((t.eTruncLT.obj ⊤).map ((t.eTruncLTι b).app X))

Tactic:
obtain rfl : b = ⊤ := by simpa using h

Premises used: rfl
-- 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
X : C
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:
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 : 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))
top : ∀ (h : ⊤ ≤ b), IsIso ((t.eTruncLT.obj ⊤).map ((t.eTruncLTι b).app X))
⊢ IsIso ((t.eTruncLT.obj 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

Premises used: rfl
-- 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 : EInt
X : C
⊢ a ≤ a

Tactic:
rfl
-- 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 : EInt
X : C
rw : IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))
⊢ IsIso (X := (t.eTruncLT.obj a).obj ((t.eTruncLT.obj a).obj X)) ((t.eTruncLTι a).app ((t.eTruncLT.obj a).obj X))

Tactic:
rw [← eTruncLT_obj_map_eTruncLTι_app]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_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 : EInt
X : C
⊢ IsIso ((t.eTruncLT.obj a).map ((t.eTruncLTι a).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
X : C
n : ℤ
inst_7 : t.IsGE X n
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.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
X : C
n : ℤ
inst_7 : t.IsGE X n
⊢ t.IsGE ((t.eTruncLT.obj ⊥).obj X) n

Tactic:
exact isGE_of_isZero _ (by simp) _

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_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
X : C
n : ℤ
inst_7 : t.IsGE X n
a : ℤ
coe : t.IsGE ((t.truncLT a).obj X) n
⊢ t.IsGE ((t.eTruncLT.obj (WithBotTop.coe a)).obj X) n

Tactic:
dsimp
-- 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
X : C
n : ℤ
inst_7 : t.IsGE X n
a : ℤ
⊢ t.IsGE ((t.truncLT a).obj X) n

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
X : C
n : ℤ
inst_7 top : t.IsGE X n
⊢ t.IsGE ((t.eTruncLT.obj ⊤).obj X) n

Tactic:
dsimp
-- 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
X : C
n : ℤ
inst_7 : t.IsGE X n
⊢ t.IsGE X n

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
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
top : t.IsGE ((t.eTruncLT.obj ⊤).obj X) n
⊢ t.IsGE ((t.eTruncLT.obj i).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

Premises used: CategoryTheory.Triangulated.TStructure.isGE_of_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
X : C
n : ℤ
inst_7 bot : t.IsLE X n
⊢ t.IsLE ((t.eTruncGE.obj ⊥).obj X) n

Tactic:
dsimp
-- 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
X : C
n : ℤ
inst_7 : t.IsLE X n
⊢ t.IsLE X n

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
X : C
n : ℤ
inst_7 : t.IsLE X n
a : ℤ
coe : t.IsLE ((t.truncGE a).obj X) n
⊢ t.IsLE ((t.eTruncGE.obj (WithBotTop.coe a)).obj X) n

Tactic:
dsimp
-- 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
X : C
n : ℤ
inst_7 : t.IsLE X n
a : ℤ
⊢ t.IsLE ((t.truncGE a).obj X) n

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
X : C
n : ℤ
inst_7 : t.IsLE X n
⊢ IsZero.{v_1, u_1} ((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
X : C
n : ℤ
inst_7 : t.IsLE X n
⊢ t.IsLE ((t.eTruncGE.obj ⊤).obj X) n

Tactic:
exact isLE_of_isZero _ (by simp) _

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_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
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
top : t.IsLE ((t.eTruncGE.obj ⊤).obj X) n
⊢ t.IsLE ((t.eTruncGE.obj i).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) _

Premises used: CategoryTheory.Triangulated.TStructure.isLE_of_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 : EInt
hab : a ≤ b
rw : ∀ (X : C), IsIso ((t.eTruncGEToGEGE a b).app X)
⊢ IsIso (t.eTruncGEToGEGE 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 : EInt
hab : a ≤ b
X : C
simp : IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
⊢ IsIso ((t.eTruncGEToGEGE a b).app X)

Tactic:
simp only [Functor.comp_obj, eTruncGEToGEGE_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_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 : EInt
hab : a ≤ b
X : C
⊢ IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))

Tactic:
t.isIso_eTruncGE_obj_map_truncGEπ_app _ _ hab _

Premises used: CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_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 : EInt
hab : a ≤ b
X : C
⊢ IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))

Tactic:
exact t.isIso_eTruncGE_obj_map_truncGEπ_app _ _ hab _

Premises used: CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_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 : EInt
hab : a ≤ b
X : C
⊢ (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) ≫ (t.eTruncGEIsoGEGE a b hab).inv.app X =
    𝟙 ((t.eTruncGE.obj b).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X))

Tactic:
simpa using (t.eTruncGEIsoGEGE a b hab).hom_inv_id_app X

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE
-- 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
hab : a ≤ b
X : C
⊢ (t.eTruncGEIsoGEGE a b hab).inv.app X ≫ (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X) =
    𝟙 ((t.eTruncGE.obj a ⋙ t.eTruncGE.obj b).obj X)

Tactic:
simpa using (t.eTruncGEIsoGEGE a b hab).inv_hom_id_app X

Premises used: CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE, CategoryTheory.Iso.inv_hom_id_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 : EInt
hab : b ≤ a
rw : ∀ (X : C), IsIso ((t.eTruncLTLTToLT a b).app X)
⊢ IsIso (t.eTruncLTLTToLT 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 : EInt
hab : b ≤ a
X : C
simp : IsIso ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X))
⊢ IsIso ((t.eTruncLTLTToLT a b).app X)

Tactic:
simp only [Functor.comp_obj, eTruncLTLTToLT_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_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 : EInt
hab : b ≤ a
X : C
⊢ IsIso ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X))

Tactic:
t.isIso_eTruncLT_obj_map_truncLTπ_app _ _ hab _

Premises used: CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_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 : EInt
hab : b ≤ a
X : C
⊢ IsIso ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X))

Tactic:
exact t.isIso_eTruncLT_obj_map_truncLTπ_app _ _ hab _

Premises used: CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_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 : EInt
hab : b ≤ a
X : C
⊢ (t.eTruncLT.obj b).map ((t.eTruncLTι a).app X) ≫ (t.eTruncLTLTIsoLT a b hab).inv.app X =
    𝟙 ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))

Tactic:
simpa using (t.eTruncLTLTIsoLT a b hab).hom_inv_id_app X

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT
-- 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
hab : b ≤ a
X : C
⊢ (t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X) ≫
      (t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X)) =
    𝟙 ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))

Tactic:
simp [eTruncLT_obj_map_eTruncLTι_app]

Premises used: CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_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 : EInt
rw : ∀ (X : C), IsIso ((t.eTruncLTGELTSelfToLTGE a b).app X)
⊢ IsIso (t.eTruncLTGELTSelfToLTGE 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 : EInt
X : C
⊢ IsIso (X := (t.eTruncLT.obj ⊥ ⋙ t.eTruncGE.obj a ⋙ t.eTruncLT.obj ⊥).obj X)
    (NatTrans.app (t.eTruncLTGELTSelfToLTGE a ⊥) X)

Tactic:
simp [isIsoZero_iff_source_target_isZero]

Premises used: CategoryTheory.Limits.isIsoZero_iff_source_target_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 : ℤ
⊢ 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:
simpa using inferInstanceAs (IsIso ((t.truncLT b).map ((t.truncLTι b).app X)))