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
n : ℤ
X : C
i : ℤ
h : i ≤ n + 1
⊢ i - 1 ≤ n

Tactic:
lia
-- 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
n : ℤ
X : C
i : ℤ
h : i ≤ n + 1
⊢ t.IsLE ((t.truncLT i).obj X) n

Tactic:
exact t.isLE_of_le _ (i - 1) n (by lia)

Premises used: HSub.hSub, CategoryTheory.Triangulated.TStructure.isLE_of_le, OfNat.ofNat
-- 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
n : ℤ
X : C
h : ⊤ ≤ WithBotTop.coe (n + 1)
⊢ t.IsLE ((t.eTruncLT.obj ⊤).obj X) n

Tactic:
simp at 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
n : ℤ
i : EInt
h : i ≤ WithBotTop.coe (n + 1)
X : C
bot : ∀ (h : ⊥ ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj ⊥).obj X) n
coe : ∀ (i : ℤ) (h : WithBotTop.coe i ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj (WithBotTop.coe i)).obj X) n
top : ∀ (h : ⊤ ≤ WithBotTop.coe (n + 1)), t.IsLE ((t.eTruncLT.obj ⊤).obj X) n
⊢ t.IsLE ((t.eTruncLT.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with
  | bot => exact t.isLE_of_isZero (by simp) _
  | coe i =>
    simp only [WithBotTop.coe_le_coe] at h
    dsimp
    exact t.isLE_of_le _ (i - 1) n (by lia)
  | top => simp at h

Premises used: WithBotTop.coe_le_coe, HSub.hSub, CategoryTheory.Triangulated.TStructure.isLE_of_isZero, CategoryTheory.Triangulated.TStructure.isLE_of_le, OfNat.ofNat
-- 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
X : C
n : ℤ
inst_6 : t.IsGE X n
hj : ⊥ ≤ WithBotTop.coe 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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : ℤ
hj : WithBotTop.coe j ≤ WithBotTop.coe n
⊢ j ≤ n

Tactic:
simpa using hj
-- 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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : ℤ
hj : WithBotTop.coe j ≤ WithBotTop.coe n
⊢ t.IsGE X j

Tactic:
have := t.isGE_of_ge X j n (by simpa using hj)
-- 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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : ℤ
hj : WithBotTop.coe j ≤ WithBotTop.coe n
this : t.IsGE X j
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj (WithBotTop.coe j)).obj X)

Tactic:
t.isZero_truncLT_obj_of_isGE _ _

Premises used: CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE
-- 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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : ℤ
hj : WithBotTop.coe j ≤ WithBotTop.coe n
this : t.IsGE X j
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj (WithBotTop.coe j)).obj X)

Tactic:
exact t.isZero_truncLT_obj_of_isGE _ _

Premises used: CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE
-- 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
X : C
n : ℤ
inst_6 : t.IsGE X n
hj : ⊤ ≤ WithBotTop.coe n
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊤).obj X)

Tactic:
simp at hj
-- 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
X : C
n : ℤ
inst_6 : t.IsGE X n
j : EInt
hj : j ≤ WithBotTop.coe n
bot : ∀ (hj : ⊥ ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊥).obj X)
coe :
  ∀ (j : ℤ) (hj : WithBotTop.coe j ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj (WithBotTop.coe j)).obj X)
top : ∀ (hj : ⊤ ≤ WithBotTop.coe n), IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊤).obj X)
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj j).obj X)

Tactic:
induction j using WithBotTop.rec with
  | bot => simp
  | coe j =>
    have := t.isGE_of_ge X j n (by simpa using hj)
    exact t.isZero_truncLT_obj_of_isGE _ _
  | top => simp at hj

Premises used: CategoryTheory.Triangulated.TStructure.isZero_truncLT_obj_of_isGE
-- 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
X : C
n : ℤ
inst_6 : t.IsLE X n
hj : WithBotTop.coe n < ⊥
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊥).obj X)

Tactic:
simp at hj
-- 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
X : C
n : ℤ
inst_6 : t.IsLE X n
j : ℤ
hj : WithBotTop.coe n < WithBotTop.coe j
⊢ n < j

Tactic:
simp only [WithBotTop.coe_lt_coe] at hj

Premises used: WithBotTop.coe_lt_coe
-- 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
X : C
n : ℤ
inst_6 : t.IsLE X n
j : ℤ
hj : n < j
⊢ n ≤ j - 1

Tactic:
lia
-- 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
X : C
n : ℤ
inst_6 : t.IsLE X n
j : ℤ
hj : n < j
⊢ t.IsLE X (j - 1)

Tactic:
have := t.isLE_of_le X n (j - 1) (by lia)
-- 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
X : C
n : ℤ
inst_6 : t.IsLE X n
j : ℤ
hj : n < j
this : t.IsLE X (j - 1)
⊢ j - 1 + 1 = j

Tactic:
lia
-- 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
X : C
n : ℤ
inst_6 : t.IsLE X n
j : ℤ
hj : n < j
this : t.IsLE X (j - 1)
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)

Tactic:
exact t.isZero_truncGE_obj_of_isLE (j - 1) j (by lia) _

Premises used: CategoryTheory.Triangulated.TStructure.isZero_truncGE_obj_of_isLE, HSub.hSub, OfNat.ofNat
-- 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
X : C
n : ℤ
inst_6 : t.IsLE X n
hj : WithBotTop.coe 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
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)
top : ∀ (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)

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

Premises used: WithBotTop.coe_lt_coe
-- 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
h : a ≤ ⊥
⊢ a = ⊥

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
a : EInt
X : C
h : a ≤ ⊥
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))
⊢ IsIso ((t.eTruncGE.obj ⊥).map ((t.eTruncGEπ a).app X))

Tactic:
obtain rfl : a = ⊥ := 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 (Y := (t.eTruncGE.obj ⊥).obj ((t.eTruncGE.obj ⊥).obj X))
    ((t.eTruncGE.obj ⊥).map (NatTrans.app (t.eTruncGEπ ⊥) 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
b : ℤ
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:
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
b a : ℤ
h : WithBotTop.coe a ≤ WithBotTop.coe b
⊢ a ≤ 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
X : C
b 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:
exact t.isIso_truncGE_map_truncGEπ_app b a (by simpa using h) X

Premises used: CategoryTheory.Triangulated.TStructure.isIso_truncGE_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
X : C
b : ℤ
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:
simp at 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
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))
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))

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
-- 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
h : a ≤ ⊤
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊤).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) 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 : EInt
X : C
h : a ≤ ⊤
⊢ IsZero.{v_1, u_1} ((t.eTruncGE.obj ⊤).obj ((t.eTruncGE.obj a).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 : EInt
X : C
h : a ≤ ⊤
⊢ IsIso ((t.eTruncGE.obj ⊤).map ((t.eTruncGEπ a).app X))

Tactic:
exact ⟨0, IsZero.eq_of_src (by simp) _ _, 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 : 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))
top : ∀ (h : a ≤ ⊤), IsIso ((t.eTruncGE.obj ⊤).map ((t.eTruncGEπ a).app X))
⊢ IsIso ((t.eTruncGE.obj 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) _ _⟩

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
b : EInt
X : C
h : ⊥ ≤ b
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.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
b : EInt
X : C
h : ⊥ ≤ b
⊢ IsZero.{v_1, u_1} ((t.eTruncLT.obj ⊥).obj (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) 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
b : EInt
X : C
h : ⊥ ≤ b
⊢ IsIso ((t.eTruncLT.obj ⊥).map ((t.eTruncLTι b).app X))

Tactic:
exact ⟨0, IsZero.eq_of_src (by simp) _ _, 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
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))

Tactic:
simp at 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
X : C
a b : ℤ
h : WithBotTop.coe a ≤ WithBotTop.coe b
⊢ a ≤ 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
X : C
a 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:
exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X

Premises used: CategoryTheory.Triangulated.TStructure.isIso_truncLT_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
X : C
a : ℤ
h : WithBotTop.coe a ≤ ⊤
coe : IsIso ((t.truncLT a).map (𝟙 X))
⊢ 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:
dsimp