-- 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)
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)
⊢ 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