∀ {q : ℕ} (a a_1 : ZMod q),
  a = a_1 →
    ∀ [inst : NeZero q] (s s_1 : ℂ),
      s = s_1 →
        ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a s =
          ArithmeticFunction.vonMangoldt.LFunctionResidueClassAux a_1 s_1