awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
x y : EInt
f : x ⟶ 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) x :
      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 : ⊥ ⟶ 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)
Tactic: induction x using WithBotTop.rec with
    | bot =>
      induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact 0
      | top => exact 0
    | coe a =>
      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
    | top =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _
Cleared hypotheses: x, 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
x y : EInt
f : x ⟶ y
bot :
  (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)
⊢ 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) x :
      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 : (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)
Tactic: induction x using WithBotTop.rec with
    | bot =>
      induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact 0
      | top => exact 0
    | coe a =>
      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
    | top =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _
Cleared hypotheses: x, 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
x y : EInt
f : x ⟶ y
bot :
  (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)
coe :
  (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)
⊢ 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) x :
      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 : ⊤ ⟶ 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)
Tactic: induction x using WithBotTop.rec with
    | bot =>
      induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact 0
      | top => exact 0
    | coe a =>
      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
    | top =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact 0
      | top => exact 𝟙 _
Cleared hypotheses: x, 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
i : EInt
⊢ (t.eTruncLT.obj i).Additive
have bot : (t.eTruncLT.obj ⊥).Additive
Tactic: induction i using WithBotTop.rec
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
i : EInt
bot : (t.eTruncLT.obj ⊥).Additive
⊢ (t.eTruncLT.obj i).Additive
have coe : ∀ (a : ℤ), (t.eTruncLT.obj (WithBotTop.coe a)).Additive
Tactic: induction i using WithBotTop.rec
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
i : EInt
bot : (t.eTruncLT.obj ⊥).Additive
coe : ∀ (a : ℤ), (t.eTruncLT.obj (WithBotTop.coe a)).Additive
⊢ (t.eTruncLT.obj i).Additive
have top : (t.eTruncLT.obj ⊤).Additive
Tactic: induction i using WithBotTop.rec
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasShift.{v_1, u_1, 0} C ℤ
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
t : TStructure.{v_1, u_1} C
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) (𝟭 C) t.truncGE 0 ⊥ :
      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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0 ⊥ :
      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) (𝟭 C) t.truncGE 0 ⊥ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact t.truncGEπ b
      | 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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0 ⊥ :
      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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0
          (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 t.truncGEπ b
      | 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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0 ⊥ :
          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) (𝟭 C) t.truncGE 0
            (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) (𝟭 C) t.truncGE 0 ⊥ :
      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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0 ⊥ :
      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) (𝟭 C) t.truncGE 0 ⊤ :
      Functor.{v_1, v_1, u_1, u_1} C C)
Tactic: induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact t.truncGEπ b
      | 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) (𝟭 C) t.truncGE 0
        (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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0
        (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) (𝟭 C) t.truncGE 0 ⊥ :
      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.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | 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
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) (𝟭 C) t.truncGE 0
          (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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0
        (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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0
          (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) (𝟭 C) t.truncGE 0
          (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.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | 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
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) (𝟭 C) t.truncGE 0
          (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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0
            (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) (𝟭 C) t.truncGE 0
            (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) (𝟭 C) t.truncGE 0
        (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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0
        (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) (𝟭 C) t.truncGE 0 ⊤ :
      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.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | 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
⊢ 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) (𝟭 C) t.truncGE 0 ⊤ :
      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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0 ⊤ :
      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) (𝟭 C) t.truncGE 0 ⊥ :
      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) (𝟭 C) t.truncGE 0 ⊤ :
        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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0 ⊤ :
      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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0 ⊤ :
        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) (𝟭 C) t.truncGE 0
          (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) (𝟭 C) t.truncGE 0 ⊤ :
        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) (𝟭 C) t.truncGE 0 ⊥ :
        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) (𝟭 C) t.truncGE 0 ⊤ :
          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) (𝟭 C) t.truncGE 0
            (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) (𝟭 C) t.truncGE 0 ⊤ :
      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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0 ⊤ :
      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) (𝟭 C) t.truncGE 0 ⊤ :
      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