awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X : C
n a n' : ℤ
hn' : a + n' = n
mp : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' → t.IsGE X n
⊢ t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n' ↔ t.IsGE X n
have mpr : t.IsGE X n → t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C a) X) n'
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
⊢ f = 0
have this : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
Tactic: have := t.isLE_shift X n₀ n₀ 0 (add_zero n₀)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
⊢ f = 0
have this₁ : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
Tactic: have := t.isGE_shift Y n₁ n₀ (n₁ - n₀)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
⊢ f = 0
have this₁ : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
Tactic: have := t.isGE_of_ge (Y⟦n₀⟧) 1 (n₁ - n₀)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
⊢ f = 0
have a : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
  (Functor.map (shiftFunctor C n₀) f) (Functor.map (shiftFunctor C n₀) 0)
Tactic: apply (shiftFunctor C n₀).map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
    (Functor.map (shiftFunctor C n₀) f) (Functor.map (shiftFunctor C n₀) 0)
have a : Eq (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
  (Functor.map (shiftFunctor C n₀) f) 0
Tactic: simp only [Functor.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
    (Functor.map (shiftFunctor C n₀) f) 0
have a : t.le 0 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X)
Tactic: apply t.zero'
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE Y n₁
this_1 : t.IsLE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X) 0
this_2 : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) (n₁ - n₀)
this : t.IsGE (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y) 1
a : t.le 0 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X)
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
    (Functor.map (shiftFunctor C n₀) f) 0
have a₁ : t.ge 1 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n₀) Y)
Tactic: apply t.zero'
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
X : C
n₀ n₁ : ℤ
h : n₀ < n₁
inst_6 : t.IsLE X n₀
inst_7 : t.IsGE X n₁
⊢ IsZero.{v_1, u_1} X
have rw : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: rw [IsZero.iff_id_eq_zero]
-- 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
y : EInt
f : ⊥ ⟶ y
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have bot : (f : Quiver.Hom (V := EInt) ⊥ ⊥) →
  Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact 0
      | top => exact 0
Cleared hypotheses: y, f
-- 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
y : EInt
f : ⊥ ⟶ y
bot :
  (f : Quiver.Hom (V := EInt) ⊥ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have bot₁ : (b : ℤ) →
  (f : ⊥ ⟶ WithBotTop.coe b) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
          (WithBotTop.coe b) :
        Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact 0
      | top => exact 0
Cleared hypotheses: y, f
-- 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
y : EInt
f : ⊥ ⟶ y
bot :
  (f : Quiver.Hom (V := EInt) ⊥ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
bot₁ :
  (b : ℤ) →
    (f : ⊥ ⟶ WithBotTop.coe b) →
      Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
          Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
            (WithBotTop.coe b) :
          Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have bot₂ : (f : Quiver.Hom (V := EInt) ⊥ ⊤) →
  Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact 0
      | top => exact 0
Cleared hypotheses: y, f
-- 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
y : EInt
a : ℤ
f : WithBotTop.coe a ⟶ y
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have coe : (f : WithBotTop.coe a ⟶ ⊥) →
  Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncLTOfLE a b (by simpa using leOfHom f)
      | top => exact t.truncLTι a
Cleared hypotheses: y, f
-- 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
y : EInt
a : ℤ
f : WithBotTop.coe a ⟶ y
coe :
  (f : WithBotTop.coe a ⟶ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
          (WithBotTop.coe a) :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have coe₁ : (b : ℤ) →
  (f : WithBotTop.coe a ⟶ WithBotTop.coe b) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
          (WithBotTop.coe a) :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
          (WithBotTop.coe b) :
        Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncLTOfLE a b (by simpa using leOfHom f)
      | top => exact t.truncLTι a
Cleared hypotheses: y, f
-- 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
y : EInt
a : ℤ
f : WithBotTop.coe a ⟶ y
coe :
  (f : WithBotTop.coe a ⟶ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
          (WithBotTop.coe a) :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
coe₁ :
  (b : ℤ) →
    (f : WithBotTop.coe a ⟶ WithBotTop.coe b) →
      Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
            (WithBotTop.coe a) :
          Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
            (WithBotTop.coe b) :
          Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have coe₂ : (f : WithBotTop.coe a ⟶ ⊤) →
  Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
        (WithBotTop.coe a) :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncLTOfLE a b (by simpa using leOfHom f)
      | top => exact t.truncLTι a
Cleared hypotheses: y, f
-- 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
y : EInt
f : ⊤ ⟶ y
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have top : (f : Quiver.Hom (V := EInt) ⊤ ⊥) →
  Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _
Cleared hypotheses: y, f
-- 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
y : EInt
f : ⊤ ⟶ y
top :
  (f : Quiver.Hom (V := EInt) ⊤ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have top₁ : (b : ℤ) →
  (f : ⊤ ⟶ WithBotTop.coe b) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
          (WithBotTop.coe b) :
        Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _
Cleared hypotheses: y, f
-- 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
y : EInt
f : ⊤ ⟶ y
top :
  (f : Quiver.Hom (V := EInt) ⊤ ⊥) →
    Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
        Functor.{v_1, v_1, u_1, u_1} C C)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊥ :
        Functor.{v_1, v_1, u_1, u_1} C C)
top₁ :
  (b : ℤ) →
    (f : ⊤ ⟶ WithBotTop.coe b) →
      Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
          Functor.{v_1, v_1, u_1, u_1} C C)
        (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C)
            (WithBotTop.coe b) :
          Functor.{v_1, v_1, u_1, u_1} C C)
⊢ Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) y :
      Functor.{v_1, v_1, u_1, u_1} C C)
have top₂ : (f : Quiver.Hom (V := EInt) ⊤ ⊤) →
  Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) 0 t.truncLT (𝟭 C) ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _
Cleared hypotheses: y, f