{N : ℕ} →
  [inst : NeZero N] →
    {motive : DirichletCharacter.BadChar✝ N → Sort u} →
      ((χ : DirichletCharacter ℂ N) →
          (χ_ne : χ ≠ 1) →
            (χ_sq : χ ^ 2 = 1) →
              (hχ : DirichletCharacter.LFunction χ 1 = 0) → motive { χ := χ, χ_ne := χ_ne, χ_sq := χ_sq, hχ := hχ }) →
        (t : DirichletCharacter.BadChar✝ N) → motive t