-- 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 z : EInt
g : y ⟶ z
g' : y ≤ z
f : ⊤ ⟶ y
f' : ⊤ ≤ y
top :
  ∀ (g : ⊥ ⟶ z) (g' : ⊥ ≤ z) (f : Quiver.Hom (V := EInt) ⊤ ⊥) (f' : LE.le (α := EInt) ⊤ ⊥),
    Eq (α :=
      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 z :
          Functor.{v_1, v_1, u_1, u_1} C C))
      (WithBotTop.rec (motive := fun {x : EInt} ↦
          (f : x ⟶ z) →
            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
                  z :
                Functor.{v_1, v_1, u_1, u_1} C C))
          (fun (f : ⊥ ⟶ z) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊥))
              (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) z f)
          (fun (a : ℤ) (f : WithBotTop.coe a ⟶ z) ↦
            WithBotTop.rec (motive := fun {y : EInt} ↦
              (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))
              (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
              (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b ⋯)
              (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) z f)
          (fun (f : ⊤ ⟶ z) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊤))
              z f)
          ⊤ (f ≫ g) :
        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 z :
            Functor.{v_1, v_1, u_1, u_1} C C))
      (CategoryStruct.comp (Y :=
          WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 ⊥)
          (WithBotTop.rec (motive := fun {x : EInt} ↦
            (f : x ⟶ ⊥) →
              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
                    ⊥ :
                  Functor.{v_1, v_1, u_1, u_1} C C))
            (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
              WithBotTop.rec (motive := fun {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))
                (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
                  𝟙
                    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C)
                      t.truncGE 0 ⊥))
                (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) ⊥ f)
            (fun (a : ℤ) (f : WithBotTop.coe a ⟶ ⊥) ↦
              WithBotTop.rec (motive := fun {y : EInt} ↦
                (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))
                (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
                (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b ⋯)
                (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) ⊥ f)
            (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦
              WithBotTop.rec (motive := fun {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))
                (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
                (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
                  𝟙
                    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C)
                      t.truncGE 0 ⊤))
                ⊥ f)
            ⊤ f)
          (WithBotTop.rec (motive := fun {x : EInt} ↦
            (f : x ⟶ z) →
              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
                    z :
                  Functor.{v_1, v_1, u_1, u_1} C C))
            (fun (f : ⊥ ⟶ z) ↦
              WithBotTop.rec (motive := fun {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))
                (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
                  𝟙
                    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C)
                      t.truncGE 0 ⊥))
                (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) z f)
            (fun (a : ℤ) (f : WithBotTop.coe a ⟶ z) ↦
              WithBotTop.rec (motive := fun {y : EInt} ↦
                (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))
                (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
                (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b ⋯)
                (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) z f)
            (fun (f : ⊤ ⟶ z) ↦
              WithBotTop.rec (motive := fun {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))
                (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
                (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
                  𝟙
                    (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C)
                      t.truncGE 0 ⊤))
                z f)
            ⊥ g) :
        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 z :
            Functor.{v_1, v_1, u_1, u_1} C C))
⊢ Eq (α :=
    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 z :
        Functor.{v_1, v_1, u_1, u_1} C C))
    (WithBotTop.rec (motive := fun {x : EInt} ↦
        (f : x ⟶ z) →
          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 z :
              Functor.{v_1, v_1, u_1, u_1} C C))
        (fun (f : ⊥ ⟶ z) ↦
          WithBotTop.rec (motive := fun {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))
            (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
              𝟙
                (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
                  ⊥))
            (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) z f)
        (fun (a : ℤ) (f : WithBotTop.coe a ⟶ z) ↦
          WithBotTop.rec (motive := fun {y : EInt} ↦
            (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))
            (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
            (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b ⋯)
            (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) z f)
        (fun (f : ⊤ ⟶ z) ↦
          WithBotTop.rec (motive := fun {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))
            (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
            (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
              𝟙
                (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
                  ⊤))
            z f)
        ⊤ (f ≫ g) :
      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 z :
          Functor.{v_1, v_1, u_1, u_1} C C))
    (CategoryStruct.comp (Y :=
        WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0 y)
        (WithBotTop.rec (motive := fun {x : 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))
          (fun (f : ⊥ ⟶ y) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊥))
              (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) y f)
          (fun (a : ℤ) (f : WithBotTop.coe a ⟶ y) ↦
            WithBotTop.rec (motive := fun {y : EInt} ↦
              (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))
              (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
              (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b ⋯)
              (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) y f)
          (fun (f : ⊤ ⟶ y) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊤))
              y f)
          ⊤ f)
        (WithBotTop.rec (motive := fun {x : EInt} ↦
          (f : x ⟶ z) →
            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
                  z :
                Functor.{v_1, v_1, u_1, u_1} C C))
          (fun (f : ⊥ ⟶ z) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊥))
              (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) z f)
          (fun (a : ℤ) (f : WithBotTop.coe a ⟶ z) ↦
            WithBotTop.rec (motive := fun {y : EInt} ↦
              (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))
              (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
              (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b ⋯)
              (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) z f)
          (fun (f : ⊤ ⟶ z) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊤))
              z f)
          y g) :
      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 z :
          Functor.{v_1, v_1, u_1, u_1} C C))
have top₁ : ∀ (a : ℤ) (g : WithBotTop.coe a ⟶ z) (g' : WithBotTop.coe a ≤ z) (f : ⊤ ⟶ WithBotTop.coe a) (f' : ⊤ ≤ WithBotTop.coe a),
  Eq (α :=
    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 z :
        Functor.{v_1, v_1, u_1, u_1} C C))
    (WithBotTop.rec (motive := fun {x : EInt} ↦
        (f : x ⟶ z) →
          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 z :
              Functor.{v_1, v_1, u_1, u_1} C C))
        (fun (f : ⊥ ⟶ z) ↦
          WithBotTop.rec (motive := fun {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))
            (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
              𝟙
                (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
                  ⊥))
            (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) z f)
        (fun (a : ℤ) (f : WithBotTop.coe a ⟶ z) ↦
          WithBotTop.rec (motive := fun {y : EInt} ↦
            (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))
            (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
            (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b sorry)
            (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) z f)
        (fun (f : ⊤ ⟶ z) ↦
          WithBotTop.rec (motive := fun {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))
            (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
            (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
              𝟙
                (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
                  ⊤))
            z f)
        ⊤ (f ≫ g) :
      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 z :
          Functor.{v_1, v_1, u_1, u_1} C C))
    (CategoryStruct.comp (Y :=
        WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE 0
          (WithBotTop.coe a))
        (WithBotTop.rec (motive := fun {x : EInt} ↦
          (f : x ⟶ 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
                  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
                  (WithBotTop.coe a) :
                Functor.{v_1, v_1, u_1, u_1} C C))
          (fun (f : ⊥ ⟶ WithBotTop.coe a) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊥))
              (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0)
              (WithBotTop.coe a) f)
          (fun (a_1 : ℤ) (f : WithBotTop.coe a_1 ⟶ WithBotTop.coe a) ↦
            WithBotTop.rec (motive := fun {y : EInt} ↦
              (f : WithBotTop.coe a_1 ⟶ 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_1) :
                    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))
              (fun (f : WithBotTop.coe a_1 ⟶ ⊥) ↦ 0)
              (fun (b : ℤ) (f : WithBotTop.coe a_1 ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a_1 b sorry)
              (fun (f : WithBotTop.coe a_1 ⟶ ⊤) ↦ 0) (WithBotTop.coe a) f)
          (fun (f : ⊤ ⟶ WithBotTop.coe a) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊤))
              (WithBotTop.coe a) f)
          ⊤ f)
        (WithBotTop.rec (motive := fun {x : EInt} ↦
          (f : x ⟶ z) →
            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
                  z :
                Functor.{v_1, v_1, u_1, u_1} C C))
          (fun (f : ⊥ ⟶ z) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊥ ⊥) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊥))
              (fun (b : ℤ) (f : ⊥ ⟶ WithBotTop.coe b) ↦ t.truncGEπ b) (fun (f : Quiver.Hom (V := EInt) ⊥ ⊤) ↦ 0) z f)
          (fun (a : ℤ) (f : WithBotTop.coe a ⟶ z) ↦
            WithBotTop.rec (motive := fun {y : EInt} ↦
              (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))
              (fun (f : WithBotTop.coe a ⟶ ⊥) ↦ 0)
              (fun (b : ℤ) (f : WithBotTop.coe a ⟶ WithBotTop.coe b) ↦ t.natTransTruncGEOfLE a b sorry)
              (fun (f : WithBotTop.coe a ⟶ ⊤) ↦ 0) z f)
          (fun (f : ⊤ ⟶ z) ↦
            WithBotTop.rec (motive := fun {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))
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊥) ↦ 0) (fun (b : ℤ) (f : ⊤ ⟶ WithBotTop.coe b) ↦ 0)
              (fun (f : Quiver.Hom (V := EInt) ⊤ ⊤) ↦
                𝟙
                  (WithBotTop.rec (motive := fun (x : WithBotTop ℤ) ↦ Functor.{v_1, v_1, u_1, u_1} C C) (𝟭 C) t.truncGE
                    0 ⊤))
              z f)
          (WithBotTop.coe a) g) :
      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 z :
          Functor.{v_1, v_1, u_1, u_1} C C))
Tactic: induction y using WithBotTop.rec
Cleared hypotheses: y, g, g', f, f'