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) (𝟭 C) t.truncGE 0 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) (𝟭 C) t.truncGE 0 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) (𝟭 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)
Tactic: induction x using WithBotTop.rec with
    | bot =>
      induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact t.truncGEπ b
      | top => exact 0
    | coe a =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | top => exact 0
    | 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) (𝟭 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)
⊢ 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 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) (𝟭 C) t.truncGE 0 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) (𝟭 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)
Tactic: induction x using WithBotTop.rec with
    | bot =>
      induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact t.truncGEπ b
      | top => exact 0
    | coe a =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | top => exact 0
    | 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) (𝟭 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)
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) (𝟭 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)
⊢ 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 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) (𝟭 C) t.truncGE 0 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) (𝟭 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)
Tactic: induction x using WithBotTop.rec with
    | bot =>
      induction y using WithBotTop.rec with
      | bot => exact 𝟙 _
      | coe b => exact t.truncGEπ b
      | top => exact 0
    | coe a =>
      induction y using WithBotTop.rec with
      | bot => exact 0
      | coe b => exact t.natTransTruncGEOfLE a b (by simpa using leOfHom f)
      | top => exact 0
    | 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.eTruncGE.obj i).Additive
have bot : (t.eTruncGE.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.eTruncGE.obj ⊥).Additive
⊢ (t.eTruncGE.obj i).Additive
have coe : ∀ (a : ℤ), (t.eTruncGE.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.eTruncGE.obj ⊥).Additive
coe : ∀ (a : ℤ), (t.eTruncGE.obj (WithBotTop.coe a)).Additive
⊢ (t.eTruncGE.obj i).Additive
have top : (t.eTruncGE.obj ⊤).Additive
Tactic: induction i using WithBotTop.rec
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
a b : EInt
hab : a ⟶ b
⊢ Eq (α :=
    t.eTruncGE.obj a ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 a ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
have hab₁ : a ≤ b
Tactic: replace hab := leOfHom hab
-- 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
a b : EInt
hab_1 : a ⟶ b
hab : a ≤ b
⊢ Eq (α :=
    t.eTruncGE.obj a ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 a ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have bot : ∀ (hab : ⊥ ⟶ b) (hab_2 : ⊥ ≤ b),
  Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
Tactic: induction a using WithBotTop.rec
Cleared hypotheses: a, hab_1, hab
-- 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
a b : EInt
hab_1 : a ⟶ b
hab : a ≤ b
bot :
  ∀ (hab : ⊥ ⟶ b) (hab_2 : ⊥ ≤ b),
    Eq (α :=
      t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
      (t.eTruncGE.map hab ≫
        WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
          t.eTruncGE.obj x ⟶
            (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
          0 t.truncGEδLT 0 b)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
          t.eTruncGE.obj x ⟶
            (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
          0 t.truncGEδLT 0 ⊥ ≫
        (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
⊢ Eq (α :=
    t.eTruncGE.obj a ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 a ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have coe : ∀ (a : ℤ) (hab : WithBotTop.coe a ⟶ b) (hab_2 : WithBotTop.coe a ≤ b),
  Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
Tactic: induction a using WithBotTop.rec
Cleared hypotheses: a, hab_1, hab
-- 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
b : EInt
hab_1 : ⊥ ⟶ b
hab : ⊥ ≤ b
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have bot : ∀ (hab : Quiver.Hom (V := EInt) ⊥ ⊥) (hab_2 : LE.le (α := EInt) ⊥ ⊥),
  Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊥)
    (t.eTruncGE.map hab ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
Tactic: induction b using WithBotTop.rec
Cleared hypotheses: b, hab_1, hab
-- 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
b : EInt
hab_1 : ⊥ ⟶ b
hab : ⊥ ≤ b
bot :
  ∀ (hab : Quiver.Hom (V := EInt) ⊥ ⊥) (hab_2 : LE.le (α := EInt) ⊥ ⊥),
    Eq (α :=
      t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊥)
      (t.eTruncGE.map hab ≫
        WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
          t.eTruncGE.obj x ⟶
            (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
          0 t.truncGEδLT 0 ⊥)
      (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
          t.eTruncGE.obj x ⟶
            (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
          0 t.truncGEδLT 0 ⊥ ≫
        (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj b)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 b)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have bot₁ : ∀ (a : ℤ) (hab : ⊥ ⟶ WithBotTop.coe a) (hab_2 : ⊥ ≤ WithBotTop.coe a),
  Eq (α :=
    t.eTruncGE.obj ⊥ ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a))
    (t.eTruncGE.map hab ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a))
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
Tactic: induction b using WithBotTop.rec
Cleared hypotheses: b, hab_1, hab
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊥
hab : LE.le (α := EInt) ⊥ ⊥
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊥)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have hab₁ : True
Tactic: simp at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
a : ℤ
hab_1 : ⊥ ⟶ WithBotTop.coe a
hab : ⊥ ≤ WithBotTop.coe a
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a))
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 (WithBotTop.coe a))
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have hab₁ : True
Tactic: simp at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc (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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊤
hab : LE.le (α := EInt) ⊥ ⊤
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊤)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊤)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have hab₁ : True
Tactic: simp at hab
Cleared hypotheses: hab
-- 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
hab_1 : Quiver.Hom (V := EInt) ⊥ ⊥
hab : True
⊢ Eq (α :=
    t.eTruncGE.obj ⊥ ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj ⊥)
    (t.eTruncGE.map hab_1 ≫
      WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥)
    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦
        t.eTruncGE.obj x ⟶ (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj x)
        0 t.truncGEδLT 0 ⊥ ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have bot : Eq (α := Quiver.Hom (V := Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) (0 ⋙ shiftFunctor C (A := ℤ) 1)) (𝟙 (𝟭 C) ≫ 0)
  (0 ≫ Functor.whiskerRight (𝟙 0) (shiftFunctor C (A := ℤ) 1))
Tactic: dsimp [eTruncGE, eTruncLT]