-- 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
a : ℤ
hab_1 : WithBotTop.coe a ⟶ b
hab : WithBotTop.coe a ≤ b
coe :
  ∀ (hab : WithBotTop.coe a ⟶ ⊥) (hab_2 : WithBotTop.coe a ≤ ⊥),
    Eq (α :=
      t.eTruncGE.obj (WithBotTop.coe a) ⟶
        (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 (WithBotTop.coe a) ≫
        (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
coe₁ :
  ∀ (a_1 : ℤ) (hab : WithBotTop.coe a ⟶ WithBotTop.coe a_1) (hab_2 : WithBotTop.coe a ≤ WithBotTop.coe a_1),
    Eq (α :=
      t.eTruncGE.obj (WithBotTop.coe a) ⟶
        (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).obj (WithBotTop.coe a_1))
      (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_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) ≫
        (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab)
⊢ 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_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 (WithBotTop.coe a) ≫
      (t.eTruncLT ⋙ Functor.obj (Functor.whiskeringRight C C C) (shiftFunctor C (A := ℤ) 1)).map hab_1)
have coe₂ : ∀ (hab : WithBotTop.coe a ⟶ ⊤) (hab_2 : WithBotTop.coe a ≤ ⊤),
  Eq (α :=
    t.eTruncGE.obj (WithBotTop.coe a) ⟶
      (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 (WithBotTop.coe a) ≫
      (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