-- 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)
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)
⊢ 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 top : ∀ (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