-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : C
m n : ℤ
hmn : m + n = 0
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
          (Opposite.op X)))
    (Functor.map (shiftFunctor Cᵒᵖ m)
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m)
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
            (Opposite.op X)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X)))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n)))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X)))
        (Functor.map (shiftFunctor Cᵒᵖ n)
            (Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C m n hmn)) (Opposite.op X))))) ≫
          Functor.map (shiftFunctor Cᵒᵖ n)
              (NatTrans.app (Iso.inv (shiftFunctorOpIso C m n hmn))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))) ≫
            NatTrans.app (Iso.inv (shiftFunctorComm Cᵒᵖ n m))
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ m) (Opposite.op X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ m)
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
have obtain : ∀ (hmn : -n + n = 0),
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n))
        (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n))
        (Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
          (Opposite.op X)))
    (Functor.map (shiftFunctor Cᵒᵖ (-n))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n))) (Opposite.op X)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n))
          (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) (Opposite.op X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n))
          (Functor.obj.{v_1, v_1, u_1, u_1}
            (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
            (Opposite.op X)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, v_1, u_1, u_1}
          (Equivalence.inverse (opShiftFunctorEquivalence C n) ⋙ Equivalence.functor (opShiftFunctorEquivalence C n))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence C n)))
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)))
        (Functor.map (shiftFunctor Cᵒᵖ n)
            (Quiver.Hom.op
              (Functor.map (shiftFunctor C n)
                (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C (-n) n hmn)) (Opposite.op X))))) ≫
          Functor.map (shiftFunctor Cᵒᵖ n)
              (NatTrans.app (Iso.inv (shiftFunctorOpIso C (-n) n hmn))
                (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))) ≫
            NatTrans.app (Iso.inv (shiftFunctorComm Cᵒᵖ n (-n)))
              (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X))) :
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ)
          (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (-n)) (Opposite.op X)) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n ⋙ shiftFunctor Cᵒᵖ (-n))
          (Opposite.op (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) X)))
Tactic: obtain rfl : m = -n := by lia
Cleared hypotheses: m, hmn